proposition: Lemma semReturnEnum {A} (x : A) : semProd (ret x) <--> [set x].
proof: Proof. rewrite /semProd /semProdSize /= /semEnumSize /= bigcup_const ?codom_const //. - split; auto. + intros [Eq | Contra]; [subst; reflexivity | inversion Contra]. - do 2! constructor. Qed.
imports: ZArith List mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat) Numbers.BinNums Classes.RelationClasses ExtLib.Structures(Functor Applicative) QuickChick(Sets Tactics Producer LazyList RandomQC)