proposition: Lemma gencongr_min (r : rel word) : equivalence_rel r -> congruence_rel r -> (forall x y, y \in rule x -> r x y) -> forall x y, gencongr x y -> r x y.
proof: Proof. Proof using. move=> /equivalence_relP[Hrefl Htrans] Hcongr Hrule x y /rtransP[l]. elim: l x => [/= x _ ->| l0 l IHl] /=; first exact: Hrefl. move=> x /andP[/flatten_mapP[[[i j1] k]]]. rewrite -cat3_equiv_cut3 /= => /eqP->{x} /mapP[j2 Hj2 ->]. move=> {}/IHl /[apply]; rewrite (@Htrans _ (i ++ j2 ++ k)) //=. by apply: Hcongr; exact: Hrule. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK