proposition: Lemma notin_fv_wf : forall E (X : atom) T, wf_typ E T -> X `notin` dom E -> X `notin` fv_tt T.
proof: Proof. Proof with auto. intros E X T Wf_typ. induction Wf_typ; intros Fr; simpl... Case "wf_typ_var". assert (X0 `in` (dom E))... eapply binds_In; eauto. assert (X <> X0) by fsetdec. fsetdec. Case "wf_typ_all". apply notin_union... pick fresh Y. apply (notin_fv_tt_open Y)... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure