proposition: Lemma al_constant : forall (t : nat) (di0 cx0 al0 : BV) (mem0 : Memo), al t di0 cx0 al0 mem0 = al0.
proof: Proof. simple induction t. auto. intros. rewrite al_t. elim (IsNull (cx n di0 cx0 al0 mem0)). apply H. apply H. Qed.
imports: Fill_defs