proposition: Lemma dupl_strip : forall (X:seq (A*B)), strip (dupl X) = X.
proof: Proof. by elim => [|[hda hdb] tl hi] //=; rewrite hi. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)