proposition: Lemma extension_restr: restriction2 (extension f x y) (source f) (target f) = f.
proof: Proof. have pa: restriction2_axioms (extension f x y) (source f) (target f). have ha: function (extension f x y) by apply: extension_f. have hb: sub (source f) (source (extension f x y)). by rewrite /extension; aw; fprops. split => //; rewrite /extension; aw; fprops. move => t /(Vf_image_P ha hb) [u usf ->]; rewrite (extension_Vf_in usf); Wtac. move: (restriction2_prop pa) => [pb pc pd]. apply: function_exten => //; rewrite pc => t tx. by rewrite (restriction2_V pa tx) (extension_Vf_in tx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)