proposition: Lemma remove_nvar_cons : forall v x xs, remove_nvar (x :: xs) v = if beq_var v x then remove_nvar xs v else x :: remove_nvar xs v.
proof: Proof. unfold remove_nvar; sp. rewrite remove_nvars_cons_r; simpl. rewrite memvar_singleton. rewrite beq_var_sym; sp. Qed.
imports: list Omega