proposition: Lemma in_isort_iff A x (r : relation A) l : In x (isort r l) <-> In x l.
proof: Proof. induction l; ins; rewrite in_app_iff; ins; in_simp; rewrite IHl. tauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid