proposition: Lemma mapTotalResult_idSize {C} `{Checkable C} (f : Result -> Result) (c : C) s : (forall res, resultSuccessful res = resultSuccessful (f res)) -> (semCheckerSize (mapTotalResult f c) s <-> semCheckableSize c s).
proof: Proof. move=> eq_res. rewrite /mapTotalResult /mapRoseResult /mapProp/semCheckableSize /semCheckerSize. split; rewrite semFmapSize. - move => H1 b [[[res l]] /= [H2 H3]]. rewrite -H3 eq_res. apply H1. repeat (eexists; split; eauto). - move => /= H1 b [[[res l]] /= [[[[res' l'] [/= H2 [H3 H4]]] H5]]]; subst. rewrite <- H5, <- eq_res in *. apply H1. eexists. split; eauto. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes