proposition: Lemma simulate_error : forall D h e s, machine_step (dom h \u D) (h,e,s) = Error _ -> scoped_conf D (h,e,s) -> not (exists e0, step (decode (h,e,s)) e0).
proof: Proof. intros. simpl in *. destruct (isVal e) eqn:?. destruct s. - destruct e; try solve [inversion H]; simpl in Heqb; inversion Heqb. - destruct f eqn:?. destruct e eqn:?; try solve [inversion H]; simpl in Heqb; inversion Heqb. destruct (AtomSetProperties.In_dec). + destruct atom_fresh. inversion H. + inversion H. - destruct e; try solve [inversion H]; simpl in Heqb; inversion Heqb. destruct (get x h) eqn:?. inversion H. intros [e0 STEP]. simpl in *. rewrite apply_heap_get_none in STEP; auto. eapply no_step_stack with (e0 := var_f x); auto. intros [e0' SS]. inversion SS. eauto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas