proposition: Lemma StronglySorted_isort A (r : relation A) (TOT: strict_total_order (fun _ : A => True) r) l (ND: NoDup l) : StronglySorted r (isort r l).
proof: Proof. destruct TOT as [[IRR T] TOT]. induction l; ins; vauto. rewrite nodup_cons in *; desc. apply StronglySorted_app; ins; in_simp; eauto with hahn. econs; eauto with hahn. apply Forall_forall; ins; in_simp. all: rewrite in_isort_iff in *; desf. forward eapply TOT with (a:=x) (b:=a); try red; ins; desf; eauto. forward eapply TOT with (a:=x1) (b:=x2); try red; ins; desf; eauto. exfalso; eauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid