proposition: Lemma semCheckableResult : forall (res: Result), semCheckable res <-> resultSuccessful res.
proof: Proof. split; [move => /(_ 0) H | move => H s]; eapply semCheckableResultSize; eauto. Unshelve. constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes