proposition: Lemma sim_incl_rcongr : forall l l' k, sim_incl l l' -> sim_incl (l++k) (l'++k).
proof: Proof. move => l l' k hl. elim: k => [ | hd tl] //=. - by rewrite ! cats0. - move/sim_inclP. move/R_elim => hs. apply/sim_inclP; apply/R_elim => x. move : (hs x); clear hs. rewrite !InA_cat /=. case: (eqA_dec x hd) => //=. by move => _ _ _; rewrite orbT. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)