proposition: Lemma semCheckableGenSize: forall (P : Type) {H : Checkable P} (gen: G P) (size : nat), (semCheckableSize gen size) <-> (forall p, semProdSize gen size p -> semCheckableSize p size).
proof: Proof. move=> P H gen s. rewrite /semCheckableSize /checker /testGenProp. split. - move => /semBindGenSize Hcheck p Hgen //=; eauto. - move => Hcheck. apply semBindGenSize => a Hgen; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes