{P : Sort u_1} →
  {L : FirstOrder.Language} →
    {M : Type w} →
      {N : Type w'} →
        {inst : L.Structure M} →
          {inst_1 : L.Structure N} →
            {t : L.Hom M N} →
              {L' : FirstOrder.Language} →
                {M' : Type w} →
                  {N' : Type w'} →
                    {inst' : L'.Structure M'} →
                      {inst'_1 : L'.Structure N'} →
                        {t' : L'.Hom M' N'} →
                          L = L' →
                            M = M' →
                              N = N' →
                                inst ≍ inst' →
                                  inst_1 ≍ inst'_1 → t ≍ t' → FirstOrder.Language.Hom.noConfusionType P t t'