congr
case e_a.e_ω.hb
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✝ : Fin k
⊢ (Rew.substs v) (Rew.emb (w x✝).term) = (w x✝).operator v
no goals