DRed = mk { d : D; pf : Dred d = d }, together with associated operations and a (still incomplete) set of lemmas
DRed = mk { d : D; pf : Dred d = d }, together with associated operations
and a (still incomplete) set of lemmas

gstew5/cage,gstew5/cage