proposition: Lemma memvar_singleton : forall a b, memvar a [b] = beq_var a b.
proof: Proof. sp. unfold memvar; simpl. destruct (eq_var_dec b a); subst; sp. apply beq_var_refl. symmetry; apply not_eq_beq_var_false; sp. Qed.
imports: list Omega