exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ ⟶ □(pᵍ ⋎ qᵍ)
no goals