proposition: Lemma lincl_cons : forall (l l1:seq T) a, lincl l l1 -> lincl l (a::l1).
proof: Proof. elim => [ | hd tl hi] l1 a //=. case/andP => hhd hdtl. apply/andP; split. by rewrite in_cons hhd orbT. by apply: hi. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)