proposition: Theorem gencongr_generic_ind grel (P : word -> Prop) x : Generated_EquivCongruence grel -> P x -> (forall a b1 c b2, P (a ++ b1 ++ c) -> b2 \in rule b1 -> P (a ++ b2 ++ c)) -> forall y, grel x y -> P y.
proof: Proof. Proof using Hinvar_congr Hsym. move=> /gencongr_unique Heq Hinit Hind y. by rewrite Heq; move: y; exact: gencongr_ind. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK