proposition: Lemma cx_cx' : forall t : nat, cx t di_init cx_init al_init mem_init = cx' t di_init cx_init al_init mem_init DC_a DC_d.
proof: Proof. unfold cx' in |- *. unfold compo' in |- *. unfold cx3 in |- *. unfold cx_2_1, compo_2_1 in |- *. unfold di1, cx1, al1, mem1, ad1, da1 in |- *. simple induction t. auto. intros. rewrite cx_t. rewrite cx2_t. rewrite H. trivial. Qed.
imports: Fill_spec Fill_impl