proposition: Theorem gencongr_ind (P : word -> Prop) x : P x -> (forall a b1 c b2, P (a ++ b1 ++ c) -> b2 \in rule b1 -> P (a ++ b2 ++ c)) -> forall y, gencongr x y -> P y.
proof: Proof. Proof using. move=> Hx IH; apply: (rtrans_ind Hx) => y z Hy /flatten_mapP[[[i j1] k]]. rewrite -cat3_equiv_cut3 /= => /eqP Heqy; subst y. move=> /mapP[j2 Hj2 Hz]; subst z. exact: (@IH _ j1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK