proposition: Lemma sim_incl_cons : forall hd tl l, sim_incl (hd::tl) l = (InA l hd) && sim_incl tl l.
proof: Proof. move => hd tl l /=. case: (sim_incl tl l). - by rewrite andbT. - by rewrite andbF. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)