proposition: Lemma semReturnSizeEnum A (x : A) (s : nat) : semProdSize (ret x) s <--> [set x].
proof: Proof. rewrite /semProdSize /= /semEnumSize. simpl; split; auto. move => [Eq | []]; subst; reflexivity. 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)