simp [Semiterm.Operator.const, Empty.eq_elim]
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
c : Semiterm.Const L
⊢ ω (Semiterm.Operator.const c) = Semiterm.Operator.const c
no goals