proposition: Lemma typing_to_lc_exp : forall E e T, typing E e T -> lc_exp e.
proof: Proof. intros E e T H. induction H; eauto. pick fresh x1 for L. apply (lc_abs_exists x1). auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String