proposition: Lemma semCallback_idSize {C} `{Checkable C} (cb : Callback) (c : C) (s : nat) : semCheckerSize (callback cb c) s <-> semCheckableSize c s.
proof: Proof. rewrite /callback. split; move => H'. - apply mapTotalResult_idSize in H' => //; by move => [? ? ? ? ? ?]. - apply mapTotalResult_idSize => //; by move => [? ? ? ? ? ?]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes