proposition: Lemma mem_t : forall (t : nat) (di0 cx0 al0 : BV) (mem0 : Memo), mem (S t) di0 cx0 al0 mem0 = match IsNull (cx t di0 cx0 al0 mem0) return Memo with | true => mem t di0 cx0 al0 mem0 | false => MemoWrite (mem t di0 cx0 al0 mem0) (BV_to_nat (di t di0 cx0 al0 mem0)) (al t di0 cx0 al0 mem0) end.
proof: Proof. auto. Qed.
imports: Fill_defs