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