proposition: Lemma fresh_var_not_in : forall vars, ! LIn (fresh_var vars) vars.
proof: Proof. unfold fresh_var; introv X. generalize (sort_eqvars vars); introv H. trw_h eqvars_prop H. trw_h H X. apply fresh_var_aux_sorted_not_in in X. sp. apply sort_issorted. Qed.
imports: list Omega