proposition: Lemma fgraph_to_fun_restr f s: function f -> sub s (source f) -> restriction1 f s = fgraph_to_fun (restr (graph f) s).
proof: Proof. move => ha hb; apply:function_exten4. - by rewrite/restriction1 fgraph_to_fun_source; aw. - by apply: restriction1_fs. - apply:fgraph_to_fun_fs; fprops. - rewrite{1}/restriction1; aw => x xs. by rewrite (restriction1_V ha hb xs) fgraph_to_fun_ev LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)