proposition: Lemma apply_heap_get : forall h D x e, scoped_heap D h -> get x h = Some e -> apply_heap h (var_f x) = apply_heap h (nom_to_exp e).
proof: Proof. induction 1; intros; default_simp. - Case "x is at the current heap location". rewrite subst_exp_fresh_eq; auto. fsetdec. - Case "x is later in the heap". rewrite subst_exp_fresh_eq; auto. rewrite scoped_get with (D2:= dom h\u D ); default_simp; eauto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas