proposition: Lemma semCheckableQProp (qp : QProp) : semCheckable qp <-> successful qp.
proof: Proof. split; [move => /(_ 0) H | move => H s]; eapply semCheckableQPropSize; eauto. Unshelve. constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes