contradiction
case e_a.e_ω.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (w x).operator v) (Rew.emb &x✝)
no goals