proposition: Lemma fv_in_dom : forall G e T, typing G e T -> fv_exp e [<=] dom G.
proof: Proof. intros G e T H. induction H; simpl. - Case "typing_var". apply binds_In in H0. fsetdec. - Case "typing_abs". pick fresh x. assert (Fx : fv_exp (e ^ x) [<=] dom ([(x,T1)] ++ G)) by eauto. simpl in Fx. assert (Fy : fv_exp e [<=] fv_exp (e ^ x)) by eapply fv_exp_open_exp_wrt_exp_lower. fsetdec. - Case "typing_app". fsetdec. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1