proposition: Lemma size_CorrectST {A : Type} (P : A -> Prop) {G} {PG : Producer G} {PS: @ProducerSemantics G PG} (g : nat -> G (option A)) {Hm1 : forall s, SizeMonotonicOpt (g s)} {Hm2 : SizedMonotonicOpt g} {_ : CorrectSizedST P g} : CorrectST P (sized g).
proof: Proof. inv H. constructor. intros x. split; intros Hin. - eapply corrST0. inv Hin. inv H0. eapply semSizedSize in H2. eexists. eexists; split; eauto. - eapply corrST0 in Hin. inv Hin. inv H0. inv H1. eexists (max x0 x1). split; eauto. eapply semSizedSize. eapply Hm1; [ | eapply Hm2; [ | eassumption ]]; ssromega. Qed.
imports: String List mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) Producer Generators Enumerators Tactics Sets Classes