proposition: Lemma neql_elim : forall l1 l2, neql l1 l2 <-> (exists a, (InA l1 a && ~~ InA l2 a) \/ ( ~~ InA l1 a && InA l2 a)).
proof: Proof. rewrite /neql. move => l1 l2; split. case. case/nR_elim => a h1 h2. exists a; left. by apply/andP. case/nS_elim => b h1 h2. exists b; right; by apply/andP. case => a []. case/andP => h1 h2. left. apply/nR_elim. by exists a. case/andP => h1 h2. right. apply/nS_elim. by exists a. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)