proposition: Lemma canonical_form_sum : forall e T1 T2, value e -> typing empty e (typ_sum T1 T2) -> exists e1, e = exp_inl e1 \/ e = exp_inr e1.
proof: Proof. intros e T1 T2 Val Typ. remember empty as E. remember (typ_sum T1 T2) as T. revert T1 T2 HeqE HeqT. induction Typ; intros U1 U2 EQE EQT; subst; try solve [ inversion Val | inversion EQT | eauto ]. Case "typing_sub". inversion H; subst; eauto. inversion H0. Qed.
imports: Fsub.Fsub_LetSum_Lemmas