proposition: Lemma Lfs_exten f1 f2 x: (forall t, inc t x -> f1 t = f2 t) -> Lfs f1 x = Lfs f2 x.
proof: Proof. move => eq; apply: function_exten4. - by rewrite !Lfs_source. - apply:Lfs_surjective. - apply:Lfs_surjective. - by rewrite Lfs_source => t tx; rewrite !Lfs_V // eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)