congr 1
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))) o.term =
    ((Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb) o.term
case e_a
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ (Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term)) =
    (Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb