proposition: Lemma RC_seq x y z : f x = f y -> f (x++z) = f (y++z).
proof: Proof. elim: z x y => [|a z IHz] x y; first by rewrite !cats0. rewrite -(cat1s a) (catA x [::a]) (catA y [::a]). move/(RC_f a). exact: IHz. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)