proposition: Theorem sort_unique : forall (xs : list A) (p q : sort R xs), p = q.
proof: Proof. induction p using sort_ind'; uniqueness 1. apply lelistA_unique. Qed.
imports: Coq.Arith.Peano_dec Coq.Lists.SetoidList Lia Metalib.CoqUniquenessTac