Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_zero (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
⊢ t[0] = t
Tactic:
simp [lindenbaum_next_indexed]
State after:
no goals