proposition: Theorem Erasure: 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' /\ h = erase h'.
proof: Proof. destruct 1. eapply Erasure' in H; firstorder subst. unfold N.ICExec.history, N.ICExec.StepStar.history. eauto. auto. apply init_method_R; reflexivity. constructor. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)