proposition: Lemma simulate_done : forall D h e s, machine_step (dom h \u D) (h,e,s) = Done _ -> scoped_conf D (h,e,s) -> is_value (nom_to_exp e).
proof: Proof. intros. inversion H0; subst. simpl in *. destruct (isVal e) eqn:?. destruct s eqn:?. - destruct e; simpl in Heqb; inversion Heqb. econstructor; eauto. - destruct f eqn:?. + destruct e eqn:?; simpl; try solve [inversion H]. econstructor; eauto. - destruct e; inversion H. simpl in Heqb. destruct (get x h); inversion H. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas