proposition: Lemma semReturnGen {A} (x : A) : semProd (ret x) <--> [set x].
proof: Proof. rewrite /semProd /semProdSize /= /semGenSize /= bigcup_const ?codom_const //. exact: randomSeed_inhabited. by do 2! constructor. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)