proposition: Lemma lincl_trans : transitive lincl.
proof: Proof. rewrite /transitive => y. elim => [ | hd tl hi] z //=. case/andP => hhd htl hincl. rewrite (hi z htl hincl) andbT /=. move/linclP : hincl. by apply. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)