proposition: Lemma semCheckableBool (b : bool) : semCheckable b <-> b.
proof: Proof. split; [move => /(_ 0) H | move => H s]; eapply semCheckableBoolSize; eauto. Unshelve. constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes