proposition: Lemma qf_cps_if T D (c : fF) (t : T) (e : T) : qf c -> D t -> D e -> qf_cps D ('if c then t else e).
proof: Proof. move=> qfc Dt De k kP /=; have [qft qfe] := (kP _ Dt, kP _ De). by do !rewrite qf_simpl //. 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)