proposition: Theorem sort_is_unique : forall l1 l2, is_sorted l1 -> is_sorted l2 -> permut l1 l2 -> l1 = l2.
proof: Proof. induction l1 as [ | e1 l1 ]; intros l2 S1 S2 P. inversion P; trivial. inversion P as [ | a b l k1 k2 a_eq_b P' H1 H']; dummy e1 b a_eq_b; subst. destruct k1 as [ | a1 k1]. rewrite (IHl1 k2); trivial. inversion S1; trivial. inversion S2; trivial. assert (e1_eq_a1 : b = a1). assert (O:= o_proof); inversion O as [ _ _ AS ]; apply AS; clear O AS. apply (sorted_cons_min S1); rewrite P; left; reflexivity. apply (sorted_cons_min S2); rewrite <- P; left; reflexivity. subst a1; rewrite (IHl1 (k1 ++ b :: k2)); trivial. apply sorted_tl_sorted with b; trivial. apply sorted_tl_sorted with b; trivial. simpl in P; rewrite <- permut_cons in P; trivial. reflexivity. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)