simpa[h] using r
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
r : Δ₂ ≺[c✝] Δ₁
h : c = c✝
⊢ Δ₂ ≺[c] Δ₁
no goals