{P : Sort u} →
  {α : Type w} →
    {t : Std.Rcc.HasRcoIntersection α} →
      {α' : Type w} →
        {t' : Std.Rcc.HasRcoIntersection α'} → α = α' → t ≍ t' → Std.Rcc.HasRcoIntersection.noConfusionType P t t'