simp [operator, comp, ←Rew.hom_comp_app]
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
⊢ (o.comp w).operator v = o.operator fun x => (w x).operator v
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
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))).hom o.sentence =
    ((Rew.substs fun x => (w x).operator v).comp Rew.emb).hom o.sentence