proposition: Lemma ldisjointP : forall l1 l2, reflect (forall x, InA l1 x -> InA l2 x -> False) (ldisjoint l1 l2).
proof: Proof. rewrite /ldisjoint => l1 l2; apply: (iffP idP). - move => hm x. rewrite -(InA_eq2 x hm). rewrite lminusE. case/andP => h1 h2 h3. move: h1. by rewrite h3. - elim: l1 => [ | hd tl hi] h //=. move: (h hd). rewrite InA_hd. case: (InA l2 hd) => /=. by case; reflexivity. case: (eqA_dec hd hd) => //=. move => _ _. apply: hi => // x h1 h2. apply: (h x) => //=. by case: eqA_dec. case; by reflexivity. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)