. intro hpq;
  replace hpq := membership_iff.mp hpq;
  by_contra hC; simp [not_or] at hC;
  have ⟨hp, hq⟩ := hC;
  replace hp := membership_iff.mp $ iff_mem_neg.mpr hp;
  replace hq := membership_iff.mp $ iff_mem_neg.mpr hq;
  have : Ω.theory *⊢[L]! ⊥ := disj₃'! hp hq hpq;
  have : Ω.theory *⊬[L]! ⊥ := unprovable_falsum;
  contradiction;
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ⋎ q ∈ Ω.theory → p ∈ Ω.theory ∨ q ∈ Ω.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p q : Formula α
⊢ p ∈ Ω.theory ∨ q ∈ Ω.theory → p ⋎ q ∈ Ω.theory