proposition: Lemma semCheckableResultSize: forall (res: Result) (size: nat), semCheckableSize res size <-> resultSuccessful res.
proof: Proof. rewrite /semCheckableSize. rewrite /checker. rewrite /testResult. move => res size. split. - move => /(_ (resultSuccessful res)) H. suff : [set true] (resultSuccessful res) by move <-. apply H. eexists. split. + apply @semReturnSize; eauto with typeclass_instances. reflexivity. + reflexivity. - move => H b [qp' [/semReturnSize <- <-]] //=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes