proposition: Lemma length_di : forall t : nat, lengthbv (di t di_init cx_init al_init mem_init) = a_size.
proof: Proof. simple induction t. simpl in |- *. exact di_initsize. intros. rewrite di_t. elim (IsNull (cx n di_init cx_init al_init mem_init)). exact H. rewrite length_BV_increment. exact H. Qed.
imports: Fill_defs