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.1
this : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
⊢ False
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this✝ : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
this : 𝓓 ⊢! [⊥].conj' ⟶ [].disj'
⊢ False