proposition: Lemma Erasure': forall s1 (h: list N.CExec.Label) s2, N.CExec.StepStar.step_star s1 h s2 -> forall s1', erase_state s1' s1 -> exists (h': list N.ICExec.Label) s2', N.ICExec.StepStar.step_star s1' h' s2' /\ erase_state s2' s2 /\ h = erase h'.
proof: Proof. induction 1; simpl; intros. - exists [], s1'; split; [apply N.ICExec.StepStar.refl|auto]. - apply IHstep_star in H1; clear IHstep_star; destruct H1 as [ ? [ ] ]; intuition subst. generalize H0; intro Hdup. eapply Erasure'' in Hdup; eauto. destruct Hdup as [ ? [ ] ]; intuition subst. do 3 esplit. eapply N.ICExec.StepStar.steps; eauto. intuition. symmetry; apply erase_app. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)