proposition: Lemma exists_bind A B (x : A) (g : G B) (f : nat -> B -> G A) : Correct B g -> SizeMonotonic g -> (forall a s, SizeMonotonic (f a s)) -> (exists z s, semProd (f s z) x) -> exists s : nat, semProd (bindGen g (f s)) x.
proof: Proof. intros Hc Hs1 Hs2 He. inv He. inv H. inv H0. inv H. assert (Hin : [set : B] x0) by reflexivity. eapply Hc in Hin. inv Hin. inv H. exists x1, (Nat.max x2 x3). split. reflexivity. eapply (@semBindSize G ProducerGen _ B A). eexists. split. eapply Hs1 > [ | eassumption ]. now ssromega. eapply Hs2 > [ | eassumption ]. now 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)