Indexing.SUM
type l
and r
type n
val n : n cardinal
val inj_l : l index -> n index
val inj_r : r index -> n index
val prj : n index -> (l index, r index) either