proposition: Lemma restriction_recovers f x: function f -> sub x (source f) -> restriction f x = triple x (target f) ((graph f) \cap (x \times (target f))).
proof: Proof. by move=> ff ss; rewrite -(restriction_graph1 ff ss) /restriction; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)