proposition: Lemma invar_undupE s : all invar (undup s) = all invar s.
proof: Proof. Proof using. by apply/idP/idP => /allP H; apply/allP => x Hx; apply: H; move: Hx; rewrite mem_undup. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK