proposition: Lemma cofinite_exists : forall G e T, typing G e T -> typing_e G e T.
proof: Proof. intros. induction H; eauto. pick fresh x. eapply typing_e_abs with (x:=x); eauto. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1