proposition: Lemma S_elim : forall l l', (r_not nS) l l' <-> forall x, InA l' x -> InA l x.
proof: Proof. move => l l'; split. move => h. apply/R_elim. rewrite /r_not. move => hn. apply: h. by rewrite nS_nR_In. move/R_elim => h. move => hn. apply: h. by rewrite -nS_nR_In. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)