proposition: Lemma rule_congrrule u v : v \in rule u -> v \in congrrule u.
proof: Proof. Proof using. move=> H; apply/flatten_mapP. exists ([::], u, [::]); first by rewrite -cat3_equiv_cut3 cat0s cats0. by apply/mapP; exists v; last by rewrite cat0s cats0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK