proposition: Lemma same_graph_agrees f f': function f -> function f' -> graph f = graph f' -> agrees_on (source f) f f'.
proof: Proof. move=> ff ff' geq. have seq: (source f = source f'). by rewrite -(domain_fg ff) -(domain_fg ff') geq. rewrite /agrees_on - seq; split; fprops. move=> a /(Vf_pr3 ff); rewrite geq => aux. by rewrite -(Vf_pr ff' aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)