proposition: Lemma extension_Vf_out: Vf (extension f x y) x = y.
proof: Proof. symmetry;apply: Vf_pr; first by apply:extension_f. rewrite /extension; aw; apply: setU1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)