proposition: Lemma semCollect_idSize {C} `{Checkable C} (str : String.string) (c : C) (s : nat) : semCheckerSize (collect str c) s <-> semCheckableSize c s.
proof: Proof. by rewrite /collect semLabel_idSize. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes