proposition: Lemma semCheckableQPropSize (qp : QProp) size : semCheckableSize qp size <-> successful qp.
proof: Proof. rewrite /semCheckableSize /checker /testProp. split. - move => /(_ (successful qp)) H. suff : ([set true] (successful qp)) by move => <-. apply H. eexists. split ; last by reflexivity. apply @semReturnSize; eauto with typeclass_instances. reflexivity. - move => H b [qp' [/semReturnSize <- <-]] //=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes