fact: Fixpoint sim_incl (l l' : seq A) : bool := match l with | [::] => true | hd :: tl => match sim_incl tl l' with | true => InA l' hd | false => false end end.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)