proposition: Lemma typing_abs_exists : forall E e T1 T2 (x : atom), x `notin` dom E \u fv_exp e -> typing ([(x,T1)] ++ E) (e ^ x) T2 -> typing E (abs e) (typ_arrow T1 T2).
proof: Proof. intros. apply typing_abs with (L := dom E \u fv_exp e). intros y Fr. apply typing_rename with (x:=x); auto. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1