proposition: Lemma fsfunP f f' : f =1 f' <-> f = f'.
proof: Proof. split=> [eq_fg|->//]; apply/val_inj/fmapP => k. have := eq_fg k; rewrite /(f _) /(f' _) /=. case: fndP; case: fndP => //= kf kf'; first by move->. by move/eqP/negPn; rewrite fsfun_subproof. by move/eqP/negPn; rewrite eq_sym fsfun_subproof. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)