proposition: Lemma memvar_dmemvar : forall T v lv (ct cf:T) , (if (memvar v lv) then ct else cf) = (if (dmemvar v lv) then ct else cf).
proof: Proof. intros. cases_if as Hb; auto; cases_if as Hd ; auto; subst. apply assert_memvar in Hb. sp. apply assert_memvar_false in Hb. sp; try contradiction. Qed.
imports: list Omega