proposition: Lemma restriction_Lf f x: function f -> sub x (source f) -> restriction f x = Lf (Vf f) x (target f).
proof: Proof. move => h1 h2; move: (restriction_prop h1 h2) => [pa pb pc]. have pd: lf_axiom (Vf f) x (target f) by move => t tw; Wtac. rewrite /restriction; apply: function_exten;aww. by move => t rs; rewrite restriction_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)