proposition: Lemma insert_in : forall v vars, LIn (nvar v) (insert v vars).
proof: Proof. induction vars; simpl; sp. destruct a. destruct (lt_dec n v); simpl; sp. destruct (eq_nat_dec n v); subst; simpl; sp. Qed.
imports: list Omega