proposition: Theorem Refinement: forall (p: N.ICExec.Syntax.PProg)(h: list N.ICExec.Label), N.ICExec.history (N.ICExec.init p) h -> exists (h': list AExec.Label), AExec.history (AExec.init p) h' /\ N.ICExec.ext_hist h = AExec.ext_hist h'.
proof: Proof. intros. unfold N.ICExec.history in H. unfold N.ICExec.StepStar.history in H. destruct H as [s H]. apply Refinement' in H. destruct H as [h' [s' [H1 [H2 _]]]]. exists h'. split. unfold AExec.history. unfold AExec.StepStar.history. eexists. eassumption. subv h'. symmetry. apply ext_hist_map. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)