{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toEquiv : M ≃ N) →
            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 →
              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 →
                L.Equiv M N