proposition: Lemma mapTotalResult_id {C} `{Checkable C} (f : Result -> Result) (c : C) : (forall res, resultSuccessful res = resultSuccessful (f res)) -> (semChecker (mapTotalResult f c) <-> semCheckable c).
proof: Proof. move=> eq_res; split => H' s; eapply mapTotalResult_idSize; eauto. by apply H'. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes