∀ {L : FirstOrder.Language} {M : Type u_2} {N : Type u_1} [inst : L.Structure M] (e : M ≃ N) (n : ℕ) (f : L.Functions n)
  (x : Fin n → M),
  e.toFun (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (e.toFun ∘ x)