∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (toEquiv toEquiv_1 : M ≃ N) (e_toEquiv : toEquiv = toEquiv_1)
  (map_fun' :
    ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
        FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
  (map_rel' :
    ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
      FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x),
  { toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } =
    { toEquiv := toEquiv_1, map_fun' := ⋯, map_rel' := ⋯ }