proposition: Lemma foldr_pdfs_subset l0 (s : {set T}) l s' l' : uniq l -> {subset l <= ~: s} -> foldr (fun x : T => (pdfs)^~ x) (s, l) l0 = (s', l') -> uniq l' /\ {subset l' <= ~: s'}.
proof: Proof. elim: l0 s l s' l' => /= [s l' s' l0 ? ? [<- <-]//|]. move=> x l IH s l0 s' l' uniql0 subs. case fld: (foldr _) => [s1 l1] pdfsl. have [uniql1 subs1] := IH _ _ _ _ uniql0 subs fld. have := pdfs_uniq x uniql1 subs1. rewrite pdfsl; split => //. by apply: pdfs_subset pdfsl. Qed.
imports: mathcomp(all_ssreflect) extra