proposition: Lemma sort_issorted : forall vars, issorted (sort vars).
proof: Proof. induction vars; simpl; sp. destruct a. induction IHvars; simpl; sp. constructor; simpl; sp. destruct v. destruct (lt_dec n0 n). constructor; simpl; sp. destruct x; unfold le_var. allrw in_insert; sp; subst; try omega. apply_in_hyp p. unfold le_var in p; sp. destruct (eq_nat_dec n0 n); subst; sp. constructor; simpl; sp; subst. unfold le_var; omega. apply_in_hyp p; destruct x; allunfold le_var; omega. Qed.
imports: list Omega