proposition: Lemma exists_bindOpt_Opt_Sized A B (x : A) (g : nat -> G (option B)) (f : B -> nat -> G (option A)) z : SizedMonotonicOpt g -> (forall s, SizeMonotonicOpt (g s)) -> (forall a, SizedMonotonicOpt (f a)) -> (forall a s, SizeMonotonicOpt (f a s)) -> (exists s, semProdOpt (g s) z) -> (exists s, semProdOpt (f z s) x) -> exists s : nat, semProdOpt (bindOpt (g s) (fun z => f z s)) x.
proof: Proof. intros Hs1 Hs1' Hs2 Hs2' Hg Hf. destruct Hg as [s1 He]. destruct Hf. exists (max x0 s1). eapply (@semOptBindOpt G _ _ B); eauto with typeclass_instances. inv He. inv H. inv H0. inv H1. eexists. split. eexists. split. reflexivity. eapply Hs1 > [ | eassumption ]. ssromega. eexists. split. reflexivity. eapply Hs2 > [ | eassumption ]. ssromega. 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)