proposition: Lemma gencongr_is_congr : congruence_rel gencongr.
proof: Proof. Proof using Hsym. move: gencongr_equiv => /equivalence_relP[Hrefl Htrans]. move=> a b1 c; apply: rtrans_ind. - exact: Hrefl. - move=> /= x y Hx Hrule. rewrite (@Htrans _ (a ++ x ++ c)); last apply: Hx. rewrite {Hx}; apply rule_rtrans. exact: congrrule_is_congr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK