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