proposition: Lemma typing_inv_inl : forall E e1 T, typing E (exp_inl e1) T -> forall U1 U2, sub E T (typ_sum U1 U2) -> exists S1, typing E e1 S1 /\ sub E S1 U1.
proof: Proof. Proof with eauto. intros E e1 T Typ. remember (exp_inl e1) as e. generalize dependent e1. induction Typ; intros e' EQ U1 U2 Sub; inversion EQ; subst. Case "typing_sub". eauto using (sub_transitivity T). Case "typing_inl". inversion Sub; subst... Qed.
imports: Fsub.Fsub_LetSum_Lemmas