proposition: Lemma Lfs_restriction1 f x: function f -> sub x (source f) -> restriction1 f x = Lfs (Vf f) x.
proof: Proof. move => ha hb; apply:function_exten4. - by rewrite Lfs_source /restriction1; aw. - apply: (restriction1_fs ha hb). - apply:Lfs_surjective. - rewrite{1}/restriction1; aw => t tx; rewrite (restriction1_V ha hb tx). by rewrite Lfs_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)