proposition: Lemma sim_incl_refl : forall l, sim_incl l l.
proof: Proof. elim => [ | 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)