proposition: Lemma extension_Vf_in: {inc (source f), (extension f x y) =1f f}.
proof: Proof. move=> u uf; symmetry; apply: Vf_pr; first by apply:extension_f. rewrite /extension; aw; apply: setU1_r;Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)