right
case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! p ∨ i𝓓 ⊢! q
case inr.h
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
inst✝³ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝² : ModalDisjunctive m𝓓
inst✝¹ : ModalCompanion i𝓓 m𝓓
inst✝ : S4 m𝓓
hpq : i𝓓 ⊢! p ⋎ q
this : m𝓓 ⊢! □pᵍ ⋎ □qᵍ
h : m𝓓 ⊢! qᵍ
⊢ i𝓓 ⊢! q