proposition: Lemma typing_inv_abs : forall E S1 e1 T, typing E (exp_abs S1 e1) T -> forall U1 U2, sub E T (typ_arrow U1 U2) -> sub E U1 S1 /\ exists S2, exists L, forall x, x `notin` L -> typing (x ~ bind_typ S1 ++ E) (open_ee e1 x) S2 /\ sub E S2 U2.
proof: Proof. Proof with auto. intros E S1 e1 T Typ. remember (exp_abs S1 e1) as e. generalize dependent e1. generalize dependent S1. induction Typ; intros S1 b1 EQ U1 U2 Sub; inversion EQ; subst. Case "typing_abs". inversion Sub; subst. split... exists T1. exists L... Case "typing_sub". auto using (sub_transitivity T). Qed.
imports: Fsub.Fsub_LetSum_Lemmas