proposition: Lemma read_write : forall (m : Memo) (a : addr) (v : BV), AddrOK m a -> MemoRead (MemoWrite m a v) a = MMemo v.
proof: Proof. unfold Memo, AddrOK, MemoRead, MemoWrite, MMemo in |- *. unfold MemoSize in |- *. intros. apply replace_ok; auto. Qed.
imports: Arith_compl Lists_replace BV