∀ {L : FirstOrder.Language} {M : Type u_4} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (s : L.Substructure M) {n : ℕ} (f_1 : L.Functions n) (x : Fin n → ↥s),
  (FirstOrder.Language.Embedding.codRestrict (FirstOrder.Language.Substructure.map f.toHom s) (f.domRestrict s) ⋯)
      (FirstOrder.Language.Structure.funMap f_1 x) =
    FirstOrder.Language.Structure.funMap f_1
      (⇑(FirstOrder.Language.Embedding.codRestrict (FirstOrder.Language.Substructure.map f.toHom s) (f.domRestrict s)
            ⋯) ∘
        x)