proposition: Lemma semProdSize_bigcup_isNone A s (S : set (option A)) : isNone :&: S \subset isNone :&: (\bigcup_(x in (cons (returnEnum (@None A)) nil)) semProdSize x s).
proof: Proof. intros x Hin. inv Hin. destruct x. now inv H. split; eauto. eexists. split; eauto. now left. eapply semReturnSizeEnum. 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)