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