fact: Fixpoint instr_at (C: code) (pc: Z) : option instr := match C with | nil => None | i :: C' => if pc =? 0 then Some i else instr_at C' (pc - 1) end.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)