proposition: Lemma InstExecToExec': forall h s1 s2, N.ICExec.StepStar.step_star s1 h s2 -> exists h', I.CExec.StepStar.step_star (state_map s1) h' (state_map s2) /\ inst_exec_eff_hist h = exec_eff_hist h'.
proof: Proof. intros. generalize dependent s2. generalize dependent s1. induction h as [ | l h]. intros. exists nil. split. inversion H. subst s. subst s2. constructor. apply nil_cons_end in H0. contradiction. simpl. reflexivity. intros. rename s2 into s3. apply N.ICExec.StepStar.step_star_end in H. destruct H as [s2 [N1 N2]]. specex_deprem IHh. eassumption. clear N2. destruct IHh as [h' [IHh1 IHh2]]. assert (A := InstExecToExecStep'). specex_deprem A. eassumption. destruct A as [l' [A1 A2]]. exists (l'::h'). split. apply I.CExec.StepStar.step_star_end. eexists. split; eassumption. simpl. f_equal; assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)