proposition: Lemma al_al' : forall t : nat, al t di_init cx_init al_init mem_init = al' t di_init cx_init al_init mem_init DC_a DC_d.
proof: Proof. intro. rewrite al_constant. unfold al' in |- *. unfold compo' in |- *. unfold al3 in |- *. unfold al_2_1 in |- *. unfold compo_2_1 in |- *. rewrite al2_constant. unfold al1 in |- *. trivial. Qed.
imports: Fill_spec Fill_impl