proposition: Lemma pdfs_subset s l s' l' x : uniq l -> {subset l <= ~: s} -> pdfs (s,l) x = (s', l') -> {subset l' <= ~: s'}.
proof: Proof. move=> uniql subls pdfsl. have := pdfs_correct (s,l) x (conj uniql subls). rewrite /= pdfsl. have [xins [sle [l2 [xl2 -> -> l2tsorted l2connect y]]]|_ [-> ->]//] /= := boolP (x \in s). rewrite mem_cat => /orP[yinl2|/subls/setCP nyins]. apply/setCP; move/setDP=> [ys /negP[]]; first by rewrite inE. by apply/setCP => /setDP[ys yyl2]. Qed.
imports: mathcomp(all_ssreflect) extra