proposition: Theorem gencongrP : Generated_EquivCongruence gencongr.
proof: Proof. Proof using Hsym. constructor. - exact gencongr_equiv. - exact gencongr_is_congr. - exact rule_gencongr. - exact gencongr_min. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK