proposition: Lemma enum_msetn n a : msetn n a = nseq n a :> seq K.
proof: Proof. case: n => [|n]; first by rewrite msetn0 /= enum_mset0. rewrite unlock finsupp_msetn /= enum_fsetE /= enum_fset1 /= cats0. by rewrite msetE eqxx. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap