proposition: Lemma restriction1_prop f x: function f -> sub x (source f) -> function_prop (restriction1 f x) x (Vfs f x).
proof: Proof. rewrite /restriction1 /function_prop =>ff ssf; aw; split => //. apply: function_pr; aww. rewrite Lg_range => t /funI_P [z zx ->]; apply/dirim_P; ex_tac. rewrite -/(Vf _ _); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)