tauto
case isTrue.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1
no goals