proposition: Lemma apply_heap_get_none : forall x h, get x h = None -> apply_heap h (var_f x) = var_f x.
proof: Proof. intros. alist induction h; simpl in *; auto. default_simp. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas