proposition: Lemma exists_bind_Sized_alt A B (g : nat -> G B) (f : B -> nat -> G A) (x : A) (z : B) (s' : nat) : SizedMonotonic g -> (forall s, SizeMonotonic (g s)) -> (forall a, SizedMonotonic (f a)) -> (forall a s, SizeMonotonic (f a s)) -> semProd (g s') z -> (exists s, semProd (f z s) x) -> exists s : nat, semProd (bindGen (g s) (fun x => f x s)) x.
proof: Proof. intros Hs Hs' Hsf Hsf' Hprod Hex. inv Hex. inv Hprod. inv H. destruct H0. exists (Nat.max s' x0). inv H1. exists (Nat.max x1 x2). split. reflexivity. eapply (@semBindSize G ProducerGen _ B A). eexists. split. eapply Hs > [ | eapply Hs' > [ | eassumption ] ]. ssromega. ssromega. eapply Hsf > [ | eapply Hsf' > [ | eassumption ] ]. ssromega. 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)