fact: Definition semCheckerSize (c : Checker) (s : nat): Prop := successful @: semProdSize c s \subset [set true].
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes