proposition: Lemma linclP l l' : reflect {subset l <= l'} (lincl l l').
proof: Proof. apply: (iffP idP). - elim: l => [|hd tl hi] //=. case/andP => hhd htl a; rewrite in_cons. case/orP => hu; last by apply: hi. by rewrite (eqP hu). - elim: l => [|hd tl hi] //= h. apply/andP; split; first by apply: h; rewrite in_cons eq_refl. apply/hi => a h'; apply: h. by rewrite in_cons h' orbT. Qed.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)