have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ False
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False