{P : Sort u_1} →
  {α : Sort u} →
    {x : α} →
      {β : Sort v} →
        {t : CoeDep α x β} →
          {α' : Sort u} →
            {x' : α'} →
              {β' : Sort v} → {t' : CoeDep α' x' β'} → α = α' → x ≍ x' → β = β' → t ≍ t' → CoeDep.noConfusionType P t t'