proposition: Lemma step_closed x s y : undup s =i step s -> x \in s -> rewrite_path x y -> y \in s.
proof: Proof. Proof using. move=> H Hx [] l. elim: l x Hx => [x Hx _ -> // | l0 l IHl] x Hx /= /andP[Hrule /IHl]; apply. move/(_ l0) : H; rewrite mem_undup => ->. exact: step_mem Hrule Hx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK