proposition: Lemma R_elim : forall l l', (r_not nR) l l' <-> (forall x, InA l x-> InA l' x).
proof: Proof. rewrite /r_not. move => l l'; split => h. - move => x hx. case_eq (InA l' x)=> heq => //. case: h. apply/nR_elim. exists x => //. by rewrite heq. - move/nR_elim => [b h1]. move/negP => h2. apply: h2. by apply :h . Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)