fact: Fixpoint fresh_var_aux (v : nat) (vars : list NVar) : nat := match vars with | [] => v | (nvar x) :: xs => if lt_dec v x then v else if eq_nat_dec v x then fresh_var_aux (S v) xs else fresh_var_aux v xs end.
imports: list Omega