- [x] encode-decode, decidable equality, sethood - [ ] ap and refl on the constructors - [ ] ap-ind - [ ] refl-ind - [ ] tr - [ ] lift - [ ] utr and ulift
