{P : Sort u_1} →
  {L : FirstOrder.Language} →
    {α : Type u'} →
      {a : ℕ} →
        {t : L.BoundedFormula α a} →
          {L' : FirstOrder.Language} →
            {α' : Type u'} →
              {a' : ℕ} →
                {t' : L'.BoundedFormula α' a'} →
                  L = L' → α = α' → a = a' → t ≍ t' → FirstOrder.Language.BoundedFormula.noConfusionType P t t'