proposition: Lemma function_extends_restr f x: function f -> sub x (source f) -> extends f (restriction f x).
proof: Proof. move =>ff ssf; have [pa pb pc] := (restriction_prop ff ssf). split => //; last by rewrite pc. rewrite /restriction; aw => s /funI_P [z zx ->]. by apply: Vf_pr3 => //; apply: ssf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)