proposition: Lemma extends_sV f g: extends g f -> {inc (source f), f =1f g}.
proof: Proof. move=> ext x xf; have ss:= (extends_Ssource ext). have [ff fg sg _] := ext. have pg: (inc (J x (Vf f x)) (graph g)) by apply: sg; Wtac. by rewrite (Vf_pr fg pg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)