proposition: Lemma restriction2_V f x y: restriction2_axioms f x y -> {inc x, (restriction2 f x y) =1f f}.
proof: Proof. move => ra a ax; move: (ra) => [ff sf tf sif]. rewrite /Vf/restriction2; aw. apply: sub_graph_ev; fprops;first by apply: setI2_1. by rewrite (restriction2_props ra). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)