proposition: Lemma wf_typ_open : forall E U T1 T2, uniq E -> wf_typ E (typ_all T1 T2) -> wf_typ E U -> wf_typ E (open_tt T2 U).
proof: Proof. Proof with simpl_env; eauto. intros E U T1 T2 Ok WA WU. inversion WA; subst. pick fresh X. rewrite (subst_tt_intro X)... rewrite_env (map (subst_tb X U) empty ++ E). eapply wf_typ_subst_tb... Qed.
imports: Fsub.Fsub_LetSum_Infrastructure