fact: Definition qf_red_cps T (x : cps T) (y : _ -> T) := forall e k, qf_eval e (x k) = qf_eval e (k (y e)).
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)