proposition: Lemma congrrule_is_congr : congruence_rule congrrule.
proof: Proof. Proof using. move=> a b1 c b2 /flatten_mapP[[[i j1] k]]. rewrite -cat3_equiv_cut3 /= => /eqP->{b1} /mapP[j2 Hj2 ->{b2}]. rewrite !catA [a ++ i]lock -!catA; unlock. set a1 := a ++ i; set c1 := k ++ c. apply/flatten_mapP; exists (a1, j1, c1); first by rewrite -cat3_equiv_cut3. by apply/mapP; exists j2; first exact: Hj2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK