proposition: Lemma exists_bindOpt_Opt A B (x : A) (g : G (option B)) (f : B -> nat -> G (option A)) z : SizeMonotonicOpt g -> (forall a s, SizeMonotonicOpt (f a s)) -> semProdOpt g z -> (exists s, semProdOpt (f z s) x) -> exists s : nat, semProdOpt (bindOpt g (fun x => f x s)) x.
proof: Proof. intros Hc Hs1 Hs2 He. destruct He as [s1 He]. exists s1. eapply (@semOptBindOpt G _ _ B); eauto with typeclass_instances. eexists. split; 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)