proposition: Lemma code_at_app_right2: forall C pc C1 C2 C3, code_at C pc (C1 ++ C2 ++ C3) -> code_at C (pc + codelen C1) C2.
proof: Proof. intros. apply code_at_app_right. apply code_at_app_left with (C2 := C3). rewrite app_ass; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)