proposition: Lemma restriction_prop f x: function f -> sub x (source f) -> function_prop (restriction f x) x (target f).
proof: Proof. rewrite /restriction /function_prop=> ff xs; aw; split => //. by apply: function_pr; aw; fprops; apply: restr_range. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)