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