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