proposition: Lemma semBindGenUsinzed1 {A} (gen : G A) (f : A -> Checker) `{@Unsized _ _ ProducerGen gen} : (semChecker (bindGen gen f) <-> forall a, semProd gen a -> semChecker (f a)).
proof: Proof. split; move => Hgen a. - move => [s [_ H']] s'. eapply unsized in H'. eapply semBindGenSize in Hgen; eauto. - by eapply semBindGenSize; intros; apply Hgen; eexists; split => //; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes