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