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