proposition: Lemma fresh_var_nvarx : forall vars, ! LIn nvarx vars -> fresh_var vars = nvarx.
proof: Proof. unfold fresh_var; sp. rewrite fresh_var_aux_0; sp. generalize (sort_eqvars vars); sp. alltrewrite eqvars_prop. apply_in_hyp p; sp. apply sort_issorted. Qed.
imports: list Omega