case saturated =>
  intro p;
  cases mem_lindenbaum_next_indexed t p with
  | inl h => left; simp [lindenbaum_maximal]; use (encode p + 1);
  | inr h => right; simp [lindenbaum_maximal]; use (encode p + 1);
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t∞.Saturated
no goals