induction h with
| refl => simp;
| step h ih =>
  simp [lindenbaum_next_indexed, lindenbaum_next];
  split;
  . split <;> tauto;
  . tauto;
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n : ℕ
h : m ≤ n
⊢ t[m].2 ⊆ t[n].2
no goals