proposition: Lemma code_at_app_right: forall C pc C1 C2, code_at C pc (C1 ++ C2) -> code_at C (pc + codelen C1) C2.
proof: Proof. intros. inversion H. rewrite app_ass. rewrite <- app_ass. constructor. rewrite codelen_app. subst pc. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)