proposition: Lemma apply_heap_open : forall h e e0, lc_exp e0 -> apply_heap h (open e e0) = open (apply_heap h e) (apply_heap h e0).
proof: Proof. alist induction h; intros; default_simp. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas