proposition: Lemma instr_at_code_at_nil: forall C pc i, instr_at C pc = Some i -> code_at C pc nil.
proof: Proof. induction C; cbn; intros. - discriminate. - destruct (pc =? 0) eqn:PC. + assert (pc = 0) by (apply Z.eqb_eq; auto). subst pc. change (a :: C) with (nil ++ nil ++ (a :: C)). constructor. auto. + assert (A: code_at C (pc - 1) nil) by eauto. inversion A; subst. apply code_at_intro with (C1 := a :: C1) (C3 := C3). rewrite codelen_cons. lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)