proposition: Lemma fresh_var_aux_sorted_not_in : forall vars, issorted vars -> forall n, ! LIn (nvar (fresh_var_aux n vars)) vars.
proof: Proof. intros vars H. induction H; simpl; sp. destruct v. destruct (lt_dec n n0). invs2; omega. destruct (eq_nat_dec n n0); subst. generalize (fresh_var_aux_le vs (S n0)); sp. invs2; omega. assert (n0 < n) by omega; clear n1 n2. generalize (fresh_var_aux_le vs n); sp. invs2; sp; omega. destruct v. destruct (lt_dec n n0). apply_in_hyp p. unfold le_var in p; omega. destruct (eq_nat_dec n n0); subst. allapply IHissorted; sp. allapply IHissorted; sp. Qed.
imports: list Omega