proposition: Lemma apply_heap_app : forall h e1 e2, apply_heap h (app e1 e2) = app (apply_heap h e1) (apply_heap h e2).
proof: Proof. alist induction h; default_simp. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas