{P : Sort u} →
  {α : Type} →
    {t : Std.CloseableChannel.Bounded.State✝ α} →
      {α' : Type} →
        {t' : Std.CloseableChannel.Bounded.State✝¹ α'} →
          α = α' → t ≍ t' → Std.CloseableChannel.Bounded.State.noConfusionType✝ P t t'