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