proposition: Lemma function_exten2 f f': function f -> function f' -> (f = f' <-> [/\ source f = source f', target f = target f' & agrees_on (source f) f f']).
proof: Proof. move=> ff ff'; split. by move ->;split => //; split. move => [seq teq [_ _ ag]]; apply: function_exten; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)