proposition: Lemma nS_elim : forall l l', (nS l l') <-> (exists2 x, InA l' x & ~~ InA l x).
proof: Proof. move => l l'. rewrite /nS. apply: nR_elim. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)