simp [lindenbaum_maximal]
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ ∃ i, p ∈ t[i].1