proposition: Lemma fresh_var_aux_0 : forall vars, ! LIn (nvar 0) vars -> issorted vars -> fresh_var_aux 0 vars = 0.
proof: Proof. intros nin H iss; induction iss; simpl; sp. destruct v; allsimpl. allapply not_or; sp. destruct (lt_dec 0 n); sp. destruct n; allsimpl; sp; try omega; try (provefalse; apply H; auto). Qed.
imports: list Omega