proposition: Lemma agrees_same_restriction f g x: function f -> function g -> agrees_on x f g -> target f = target g -> restriction f x = restriction g x.
proof: Proof. move=> ff fg [sf sg vfg] t. move:(restriction_prop ff sf)(restriction_prop fg sg)=>[pa pb pc][pd pe pf]. rewrite/restriction; apply:function_exten;aww => z zs. by do 2 rewrite restriction_V => //; apply: vfg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)