calc
  t₁ = ⟨t₁.tableau, t₁.saturated, t₁.consistent⟩ := by rfl;
  _  = ⟨t₂.tableau, t₂.saturated, t₂.consistent⟩ := by simp [e];
  _  = t₂                                        := by rfl;
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = t₂
no goals