proposition: Lemma tseq_correct : TS[tseq] /\ forall x, x \in tseq.
proof: Proof. suff: [/\ {subset (setT : {set T}, [::]).2 <= tseq}, TS[tseq] & forall x : T, x \in (enum T) -> x \in tseq]. case=> H1 H2 H3; split => // x. by rewrite H3 // mem_enum. rewrite /tseq; set F := foldl _; set p := (_, _). have : TS[p.2] by apply: tsorted_nil. have: p.1 = ~: [set x in p.2]. by apply/setP=> i; rewrite /= !inE. have: uniq p.2 by []. elim: (enum T) p => /= [|y l IH [s1 l1] HUl1 /= Hi Rw]. by split. have HS : {subset l1 <= ~: s1}. by move=> i; rewrite Hi !inE negbK. have := pdfs_correct (_, _) y (conj HUl1 HS). have [yIs1|yNIs1] := boolP (y \in s1); last first. case: pdfs => s2 l2 [-> ->]. have /= [Sl2 HR xI] := IH (s1,l1) HUl1 Hi Rw. split => // x. rewrite inE => /orP[/eqP->|xIl]; last by apply: xI. apply: Sl2. by move: yNIs1; rewrite Hi !inE negbK. case: pdfs => s2 l2 /= [[Ss1s2 Ul2] [l3 [yIl3 s2E l2E RWl3 Cyz]]]. case: (IH (s2, l2)) => //= [|| Sl2F RwF FI]. - by apply/setP=> i; rewrite s2E Hi l2E !inE mem_cat negb_or. - rewrite l2E; apply: (tsorted_cat Rw). apply: eq_tsorted RWl3 => i. by rewrite /= Hi !inE andbT. split=> // [i iIl1|x]; first by rewrite Sl2F // l2E mem_cat iIl1 orbT. rewrite inE => /orP[/eqP->|//]; last exact: FI. by apply: Sl2F; rewrite l2E mem_cat yIl3. Qed.
imports: mathcomp(all_ssreflect) extra