proposition: Lemma sim_incl_cat2l : forall l l' k, sim_incl l l' -> sim_incl l (l'++k).
proof: Proof. move => l l' k; elim : l => [ | hd tl ] //=. case: (sim_incl tl l') => //=. move => -> //. rewrite InA_cat. by move => ->. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)