proposition: Lemma restriction2_fs f x y: restriction2_axioms f x y -> source f = x -> Imf f = y -> surjection (restriction2 f x y).
proof: Proof. move=> ra sf iy. have [pa pb pc] := (restriction2_prop ra). split => // z; rewrite pb pc - {1} iy - {1} sf. move /(Imf_P (proj41 ra))=> [u usf uv]. ex_tac; rewrite restriction2_V //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)