proposition: Lemma RC_rep x (i j : 'I_(size x)) : i < j -> f (take i x) = f (take j x) -> f (take i x ++ drop j x) = f x.
proof: Proof. move => Hij Hfij. rewrite -{5}(cat_take_drop j x). exact: RC_seq. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)