proposition: Lemma restriction1_pr f: function f -> restriction2 f (source f) (Imf f) = restriction1 f (source f).
proof: Proof. rewrite/restriction2/restriction1=> ff. have ->: (restr (graph f) (source f) = graph f). rewrite (proj33 ff); apply: restr_to_domain; fprops. by rewrite (proj1 (setI2id_Pl _ _) (proj2 (proj31 ff))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)