proposition: Theorem gencongr_unique grel : Generated_EquivCongruence grel -> grel =2 gencongr.
proof: Proof. Proof using Hsym. move=> Hgrel x y. by apply/idP/idP; apply: gencongr_imply => //; exact gencongrP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK