proposition: Lemma typing_inv_tabs : forall E S1 e1 T, typing E (exp_tabs S1 e1) T -> forall U1 U2, sub E T (typ_all U1 U2) -> sub E U1 S1 /\ exists S2, exists L, forall X, X `notin` L -> typing (X ~ bind_sub U1 ++ E) (open_te e1 X) (open_tt S2 X) /\ sub (X ~ bind_sub U1 ++ E) (open_tt S2 X) (open_tt U2 X).
proof: Proof. Proof with simpl_env; auto. intros E S1 e1 T Typ. remember (exp_tabs S1 e1) as e. generalize dependent e1. generalize dependent S1. induction Typ; intros S1 e0 EQ U1 U2 Sub; inversion EQ; subst. Case "typing_tabs". inversion Sub; subst. split... exists T1. exists (L0 `union` L). intros Y Fr. split... rewrite_env (empty ++ Y ~ bind_sub U1 ++ E). apply (typing_narrowing S1)... Case "typing_sub". auto using (sub_transitivity T). Qed.
imports: Fsub.Fsub_LetSum_Lemmas