proposition: Lemma instr_at_app: forall i c2 c1 pc, pc = codelen c1 -> instr_at (c1 ++ i :: c2) pc = Some i.
proof: Proof. induction c1; simpl; intros; subst pc. - auto. - assert (A: codelen (a :: c1) =? 0 = false). { apply Z.eqb_neq. unfold codelen. cbn [length]. lia. } rewrite A. rewrite codelen_cons. apply IHc1. lia. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences IMP Simulation)