proposition: Lemma Inl_notl'P : forall l l', reflect (nR l l') (Inl_notl' l l').
proof: Proof. move => l l'. apply : (iffP idP). - move => h. apply/nR_elim. elim : l l' h => [ | hd tl hi] l' //=. case_eq (InA l' hd) => //=. move => hIn1 hIn2. case: (hi l' hIn2) => a ha1 ha2. exists a => //. by case: (eqA_dec a hd) => //=. move => hIn _. exists hd. case: (eqA_dec hd hd) => //=. case; by reflexivity. by rewrite hIn. - case/nR_elim => a. elim: l => [ | hd tl hi] //=. case: (eqA_dec a hd) => //=. move => heq _ hnIn. case_eq (InA l' hd) => //=. move => hIn. move/negP: hnIn. case. by rewrite (InA_eq l' heq). move => hneq hIn hnIn. case_eq (InA l' hd) => hIn2 //. by apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)