{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      {inst : L.Structure M} →
        {inst_1 : L.Structure N} →
          {P : Sort u_1} →
            {toEmbedding : M ↪ N} →
              {map_fun' :
                  autoParam
                    (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                      toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
                        FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
                    FirstOrder.Language.Embedding.map_fun'._autoParam} →
                {map_rel' :
                    autoParam
                      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                        FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔
                          FirstOrder.Language.Structure.RelMap r x)
                      FirstOrder.Language.Embedding.map_rel'._autoParam} →
                  {toEmbedding' : M ↪ N} →
                    {map_fun'' :
                        autoParam
                          (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                            toEmbedding'.toFun (FirstOrder.Language.Structure.funMap f x) =
                              FirstOrder.Language.Structure.funMap f (toEmbedding'.toFun ∘ x))
                          FirstOrder.Language.Embedding.map_fun'._autoParam} →
                      {map_rel'' :
                          autoParam
                            (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                              FirstOrder.Language.Structure.RelMap r (toEmbedding'.toFun ∘ x) ↔
                                FirstOrder.Language.Structure.RelMap r x)
                            FirstOrder.Language.Embedding.map_rel'._autoParam} →
                        { toEmbedding := toEmbedding, map_fun' := map_fun', map_rel' := map_rel' } =
                            { toEmbedding := toEmbedding', map_fun' := map_fun'', map_rel' := map_rel'' } →
                          (toEmbedding ≍ toEmbedding' → P) → P