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