proposition: Lemma semBindGenUsinzed2 {A} (gen : G A) (f : A -> Checker) `{forall a, UnsizedChecker (f a)} : (semChecker (bindGen gen f) <-> forall a, semProd gen a -> semChecker (f a)).
proof: Proof. split; move => Hgen a. - move => [s [_ H']] s'. eapply semBindGenSize in Hgen; last by eauto. eapply unsizedChecker_alt_def; 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