. intro h;
  by_contra hC; simp [not_or] at hC;
  have : p ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.1;
  have : q ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.2;
  have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
  have : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj' := t.consistent (by simp_all) (by simp_all);
  contradiction;
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1