proposition: Lemma in_insert : forall v x vars, LIn (nvar v) (insert x vars) <=> (v = x [+] LIn (nvar v) vars).
proof: Proof. induction vars; simpl; sp. split; sp; invs2; sp. destruct a. destruct (eq_nat_dec n x); subst; allsimpl. destruct (lt_dec x x); sp; try omega; allsimpl. split; sp. destruct (lt_dec n x); sp; try omega; allsimpl. trewrite IHvars; split; sp. split; sp; invs2; sp. Qed.
imports: list Omega