fact: Fixpoint lincl (l l':seq T) : bool := match l with | [::] => true | hd :: tl => (hd \in l') && (lincl tl l') end.
imports: Coq(Mergesort Permutation) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(path)