fact: Definition semCheckableSize {A} `{Checkable A} (a : A) (s : nat) : Prop := semCheckerSize (checker a) s.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes