proposition: Lemma semCheckableUnitSize (t : unit) size : semCheckableSize t size <-> True.
proof: Proof. split => // _ qp [qp' [/semReturnSize <- <-]] //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes