proposition: Lemma code_at_head: forall C pc i C', code_at C pc (i :: C') -> instr_at C pc = Some i.
proof: Proof. intros. inversion H. simpl. apply instr_at_app. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)