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