{α : Type w} →
  {P : Sort u} →
    {intersection intersection' : Std.Rci α → Std.Rco α → Std.Rco α} →
      { intersection := intersection } = { intersection := intersection' } → (intersection ≍ intersection' → P) → P