proposition: Lemma semBindGenSize {A} (gen : G A) (f : A -> Checker) (s: nat): semCheckerSize (bind gen f) s <-> forall a, semProdSize gen s a -> semCheckerSize (f a) s.
proof: Proof. unfold semCheckerSize. split. - move => H a Hsize b [qp [H1 <-]]. apply H. exists qp; split => //=. apply (@semBindSize G ProducerGen ProducerSemanticsGen). eexists; split; eauto. - move => H b [qp [/semBindSize [a [H1 H2]] <-]]. eapply H; try eassumption. eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes