proposition: Lemma semReturnGen (qp : QProp) : semChecker (ret qp) <-> semCheckable qp.
proof: Proof. split; move => H s. - by move /(_ s) /semReturnGenSize : H => //. - apply semReturnGenSize; eauto. by apply H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes