{P : Sort u_1} →
  {L : FirstOrder.Language} →
    {T : L.Theory} →
      {α : Type w} →
        {t : T.CompleteType α} →
          {L' : FirstOrder.Language} →
            {T' : L'.Theory} →
              {α' : Type w} →
                {t' : T'.CompleteType α'} →
                  L = L' → T ≍ T' → α = α' → t ≍ t' → FirstOrder.Language.Theory.CompleteType.noConfusionType P t t'