proposition: Lemma StronglySorted_eq A (r: relation A) (ORD: strict_partial_order r) l l' (SS: StronglySorted r l) (SS': StronglySorted r l') (EQ: forall x, In x l <-> In x l'): l = l'.
proof: Proof. red in ORD; desc. eapply sorted_perm_eq; eauto using NoDup_Permutation with hahn. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid