proposition: Lemma restriction2_props f x y: restriction2_axioms f x y -> domain ((graph f) \cap (x \times (target f))) = x.
proof: Proof. move=> [ff xsf ysf etc]; set_extens t. by move/funI_P => [z /setI2_P [_ /setX_P [_ h _]] ->]. move => tx; apply /domainP. by move => u /setI2_P [_] /setX_P []. exists (Vf f t); apply/setI2_P; split; [Wtac| apply: setXp_i => //; Wtac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)