proposition: Lemma remove_nvar_insert : forall vars n, remove_nvar (insert n vars) (nvar n) = remove_nvar vars (nvar n).
proof: Proof. induction vars; simpl; sp. rewrite remove_nvar_nil. rewrite remove_nvar_cons. rewrite remove_nvar_nil. rewrite <- beq_var_refl; sp. destruct a. destruct (lt_dec n0 n). rewrite remove_nvar_cons. destruct (eq_nat_dec n n0); subst; try omega. rewrite not_eq_beq_var_false; sp. rewrite remove_nvar_cons. rewrite not_eq_beq_var_false; sp. rewrite IHvars; sp. inversion H; subst; sp. inversion H; subst; sp. destruct (eq_nat_dec n0 n); subst; sp. repeat (rewrite remove_nvar_cons). rewrite <- beq_var_refl; sp. Qed.
imports: list Omega