exact ⟨d⟩
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d : { d // CutFree d }
⊢  ⊢¹! Δ
no goals