proposition: Lemma semCover_idSize {C} `{Checkable C} (b: bool) (n: nat) (str : String.string) (c : C) (s : nat) : semCheckerSize (cover b n str c) s <-> semCheckableSize c s.
proof: Proof. split. - rewrite /cover. case: b => //. move => H1. apply mapTotalResult_idSize in H1 => //. by move => [? ? ? ? ? ?]. - move => H1. rewrite /cover. case: b => //. apply mapTotalResult_idSize => //. by move => [? ? ? ? ? ?]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes