proposition: Lemma semReturnGenSize (qp : QProp) (s: nat) : semCheckerSize (ret qp) s <-> semCheckableSize qp s.
proof: Proof. rewrite /semCheckerSize. split. - move => H qp' [x [H1 H2]]. apply H. eexists; split; eauto. - move => H b [x [H1 H2]] //. apply H => //=. eexists; split; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes