proposition: Lemma machine_is_scoped: forall D h e s conf', machine_step (dom h \u D) (h,e,s) = TakeStep _ conf' -> scoped_conf D (h,e,s) -> scoped_conf D conf'.
proof: Proof. intros. simpl in H. inversion H0. subst. destruct (isVal e) eqn:?. destruct s eqn:?. - inversion H. - destruct f eqn:?. + destruct e eqn:?; try solve [inversion H]. destruct AtomSetProperties.In_dec. ++ destruct atom_fresh. inversion H; subst; clear H. simpl in *. econstructor. -- econstructor; eauto. fsetdec. -- assert (x <> x0). fsetdec. autorewrite with lngen in *. rewrite <- swap_spec; try fsetdec. rewrite fv_exp_subst_exp_upper. simpl. fsetdec. -- simpl. fsetdec. ++ inversion H; subst; clear H. simpl in *. autorewrite with lngen in *. econstructor. -- econstructor; eauto. fsetdec. -- simpl. assert ((union (add x (dom h)) D) [=] (add x (union (dom h) D))). fsetdec. rewrite H. rewrite <- H6. eapply FSetDecideTestCases.test_Subset_add_remove. -- simpl. fsetdec. - destruct e eqn:?; try solve [inversion H]. destruct (get x h) eqn:?; inversion H; subst; clear H. + split. auto. simpl in *. eapply scoped_get; eauto. fsetdec. auto. + simpl in *. inversion H; subst; clear H. econstructor. auto. fsetdec. simpl. fsetdec. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas