proposition: Lemma sub_elim : forall l l', sub l l' <-> ((forall x, InA l x -> InA l' x) /\ exists2 y, ~~InA l y & InA l' y).
proof: Proof. rewrite /sub. move => l l'; split. - case. move/nS_elim => [b h1 h2]. move/R_elim => h. split => //. by exists b. - case => h [b h1 h2]. split. apply/nS_elim. by exists b. by apply/R_elim. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)