proposition: Lemma eql_elim : forall l l', eql l l' <-> forall x, (InA l x <-> InA l' x).
proof: Proof. move => l l'; split. case. move/R_elim => h1. move/S_elim => h2. move => x; split. by apply: h1. by apply :h2. move => h. split. apply/R_elim => x hx. case: (h x). move => h' _. by apply: h'. apply/S_elim => x hx. case: (h x). move => _ h'. 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)