∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (toEquiv : M ≃ N)
  (map_fun' :
    autoParam
      (∀ {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))
      FirstOrder.Language.Equiv.map_fun'._autoParam)
  (map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam)
  (toEquiv_1 : M ≃ N)
  (map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEquiv_1.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEquiv_1.toFun ∘ x))
      FirstOrder.Language.Equiv.map_fun'._autoParam)
  (map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEquiv_1.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Equiv.map_rel'._autoParam),
  ({ toEquiv := toEquiv, map_fun' := map_fun', map_rel' := map_rel' } =
      { toEquiv := toEquiv_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 }) =
    (toEquiv = toEquiv_1)