proposition: Lemma sim_incl_cat : forall l1 l2 l, sim_incl (l1++l2) l = sim_incl l1 l && sim_incl l2 l.
proof: Proof. elim => [ | hd tl hi] l2 l //=. rewrite (hi l2 l). case: (sim_incl tl l) => //=. case: (sim_incl l2 l). by rewrite andbT. by rewrite andbF. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)