proposition: Lemma fresh_var_aux_le : forall vars v, v <= fresh_var_aux v vars.
proof: Proof. induction vars; simpl; sp. destruct a. destruct (lt_dec v n); sp. destruct (eq_nat_dec v n); subst; auto. generalize (IHvars (S n)); sp; omega. Qed.
imports: list Omega