proposition: Lemma semCover_id {C} `{Checkable C} (b: bool) (n: nat) (str : String.string) (c : C) : semChecker (cover b n str c) <-> semCheckable c.
proof: Proof. split; move => H' s; eapply semCover_idSize; first by eauto. by apply H'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes