proposition: Lemma lminusE : forall l1 l2 x, (InA (lminus l1 l2) x) = (~~ InA l2 x) && (InA l1 x).
proof: Proof. rewrite /lminus => l1 l2 x. rewrite mem_filter => //. move => a b heq. by rewrite (InA_eq l2 heq). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)