proposition: Lemma step_mem s x y : y \in rule x -> x \in s -> y \in step s.
proof: Proof. Proof using. move=> Hrule Hx. rewrite /step mem_undup mem_cat; apply/orP; right. by apply/flattenP; exists (rule x); first exact: map_f. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK