proposition: Lemma restriction_V f x: function f -> sub x (source f) -> {inc x, (restriction f x) =1f f}.
proof: Proof. by rewrite /Vf/restriction => ff ss a xa; aw; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)