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