proposition: Lemma semProdSize_bindOpt_1 A B (e : E (option A)) (f : A -> E (option B)) s : semProdSize e s None -> semProdSize (bindOpt e f) s None.
proof: Proof. unfold semProdSize; simpl. unfold semEnumSize. intros H. simpl. unfold LazyList.bindLazyList. eapply (@LazyList.lazy_concat_in (option B)). 2:{ eapply LazyList.lazy_in_map with (f := fun x : option A => Enumerators.run match x with | Some a0 => f a0 | None => returnEnum None end s) (x := None). eassumption. } simpl. now left. 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)