have : 𝓓 ⊢! [].conj' ⟶ [⊤].disj' := by simp;
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ False
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this✝ : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
this : 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
⊢ False