proposition: Lemma InstExecToExec: forall p h s, N.ICExec.StepStar.step_star (N.ICExec.init p) h s -> exists p' h' s', I.CExec.StepStar.step_star (I.CExec.init p') h' s' /\ inst_exec_eff_hist h = exec_eff_hist h'.
proof: Proof. intros. assert (A := InstExecToExec'). specex_deprem A. eassumption. destruct A as [h' [A1 A2]]. exists (fun n => prog_map (p n) n 0). exists h'. exists (state_map s). split; assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)