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