proposition: Lemma semChooseSizeEmptyEnum : forall A `{RandomQC.ChoosableFromInterval A} (a1 a2 : A), ~ (RandomQC.leq a1 a2) -> forall size, (semProdSize (choose (a1,a2)) size <--> set0).
proof: Proof. intros. simpl. intros x; split; intros H1; try now inv H1. unfold semEnumSize, chooseEnum in H1. exfalso. simpl in *. eapply H0. Abort. Lemma semSizedEnum A (f : nat -> E A) : semProd (sized f) <--> \bigcup_n semEnumSize (f n) n. Proof. by []. 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)