split
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] →
    (𝓓)-Consistent
      (match decode i with
      | some p => lindenbaum_next 𝓓 p t[i]
      | none => t[i])
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✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]