proposition: Lemma semProdSizeOpt_bicupNone A s (S : set A) : \bigcup_(x in [:: returnEnum (@None A)]) semProdSizeOpt x s \subset S.
proof: Proof. intros x Hin. inv Hin. inv H. inv H0. - inv H1. congruence. inv H. - inv H. Qed.
imports: QuickChick(QuickChick Tactics TacticsUtil Instances Classes DependentClasses Sets EnumProofs) String List micromega.Lia enumProofs mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Ltac2(Ltac2)