proposition: Lemma da2_constant : forall (t : nat) (di0 cx0 al0 : BV) (mem0 : Memo) (ad0 da0 : BV), da2 t di0 cx0 al0 mem0 ad0 da0 = da0.
proof: Proof. simple induction t. simpl in |- *; trivial. intros. rewrite da2_t. elim (IsNull (cx2 n di0 cx0 al0 mem0 ad0 da0)). apply H. apply H. Qed.
imports: Fill_defs