proposition: Theorem sort_dec : forall xs, {sort leA xs} + {~ sort leA xs}.
proof: Proof. Proof with auto. induction xs as [ | x xs [Yes | No] ]... destruct (lelistA_dec x xs)... right. intros K. inversion K... right. intros K. inversion K... Defined.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac