proposition: Lemma semProdSizeOpt_semProdOpt {A} {G : Type -> Type} {_ : Producer G} (e1 e2 : G (option A)) : (forall s, semProdSizeOpt e1 s \subset semProdSizeOpt e2 s) -> semProdOpt e1 \subset semProdOpt e2.
proof: Proof. intros H x Hin. inv Hin. inv H0. eexists. split; eauto. eapply H. eassumption. Qed.
imports: String micromega.Lia List Tactics TacticsUtil Instances Classes DependentClasses Sets Producer Generators EnumProofs Checker Decidability CheckerProofs mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Ltac2(Ltac2)