proposition: Lemma sim_incl_trans : forall l2 l1 l3, sim_incl l1 l2 -> sim_incl l2 l3 -> sim_incl l1 l3.
proof: Proof. move => l2 l1 l3. elim: l1 => [ | hd tl ] //=. case: (sim_incl tl l2) => //=. move: (@sim_incl_InA hd l2 l3). case: (sim_incl l2 l3) => //=. by move => h -> // hIn _. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)