proposition: Lemma restriction_graph1 f x: function f -> sub x (source f) -> graph (restriction f x) = (graph f) \cap (x \times (target f)).
proof: Proof. rewrite /restriction => ff xs; aw;set_extens t; last first. move/setI2_P => [tg /setX_P [pa pb pc]]; apply /funI_P; ex_tac. by apply: in_graph_Vf. move/funI_P => [z pa ->]. apply:setI2_i; first by rewrite -/(Vf _ _); Wtac. apply/setX_P; aw;split; fprops; rewrite -/(Vf _ _); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)