proposition: Lemma coll_fun_RC p q x y a : coll_fun p q x = coll_fun p q y -> coll_fun p q (x++[::a]) = coll_fun p q (y++[::a]).
proof: Proof. move => [H1 H2]. by rewrite /coll_fun !delta_cat H1 H2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)