apply lindenbaum_next_indexed_parametricConsistent_succ
case succ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i + 1]
case succ.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]