proposition: Lemma restriction2_fi f x y: injection f -> restriction2_axioms f x y -> injection (restriction2 f x y).
proof: Proof. move=> [_ fi] ra. have [pa pb pc] := (restriction2_prop ra). split => //; rewrite pb => a b ax bx. by do 2 rewrite restriction2_V=>//; apply: fi; apply: (proj42 ra). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)