proposition: Lemma sorted_perm_eq : forall A (cmp: A -> A -> Prop) (TRANS: transitive cmp) (ANTIS: antisymmetric cmp) l l' (P: Permutation l l') (S : StronglySorted cmp l) (S' : StronglySorted cmp l'), l = l'.
proof: Proof. induction l; ins. by apply Permutation_nil in P; desf. assert (X: In a l') by eauto using Permutation_in, Permutation_sym, in_eq. apply In_split2 in X; desf; apply Permutation_cons_app_inv in P. destruct l1; ins; [by inv S; inv S'; eauto using f_equal|]. assert (X: In a0 l) by eauto using Permutation_in, Permutation_sym, in_eq. inv S; inv S'; rewrite Forall_forall in *; ins. destruct X0; left; apply ANTIS; eauto with hahn. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid