cases (hMat p) with
| inl _ => assumption;
| inr h' => exact absurd h' h;
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.2
⊢ p ∈ t.1
no goals