proposition: Lemma restriction2_prop f x y: restriction2_axioms f x y -> function_prop (restriction2 f x y) x y.
proof: Proof. move=> ra; move:(ra) => [ff ss st etc]. rewrite /restriction2 /function_prop; aw; split => //. move:(restriction2_props ra); set g := _ \cap _ => dg. have fg: fgraph g. rewrite /g; apply: (@sub_fgraph _ (graph f)); fprops; apply: setI2_1. apply: function_pr=>// t tr; apply: etc; apply /dirim_P. move/(rangeP (proj1 fg)): tr => [z /setI2_P [jg /setXp_P [zx _]]];ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)