proposition: Lemma qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x).
proof: Proof. move=> ??; exact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)