apply next_parametericConsistent
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
case h_1.consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]