proposition: Lemma code_at_nil: forall C pc C1, code_at C pc C1 -> code_at C pc nil.
proof: Proof. intros. inversion H. subst. change (C1 ++ C3) with (nil ++ C1 ++ C3). constructor. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)