proposition: Lemma scoped_get : forall h D1 D2 x e, scoped_heap D1 h -> get x h = Some e -> dom h \u D1 [<=] D2 -> fv_exp (nom_to_exp e) [<=] D2.
proof: Proof. induction 1; intros; default_simp. fsetdec. eapply IHscoped_heap; auto; fsetdec. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas