proposition: Lemma types_normalizes Γ t T : Γ |-- t : T → ∃ u, Γ |-- u <= T.
proof: Proof. induction 1. exists (η (nth i Γ unit) i). apply (eta_expand Γ i (nth i Γ unit) (neutral_var _)); term. destruct IHtypes as [t' tt']. exists (λ t'); term. destruct IHtypes1 as [t' tt']. destruct IHtypes2 as [u' uu']. apply checks_arrow in tt'. destruct tt' as [t'' [t't'' t'B]]. subst. generalize (hereditary_subst_subst _ _ t'' [] Γ B uu'). destruct_call hereditary_subst. destruct o. destruct h. simpl in *. intros. destruct H1. exists t0; intuition. simpl in *. intros. destruct H1. exists t0; intuition. exists Tt; term. destruct IHtypes1 as [t' tt']. destruct IHtypes2 as [u' uu']. exists << t' , u' >>. term. destruct IHtypes as [t' tt']. depelim tt'. exists t0; term. depelim H0. destruct IHtypes as [t' tt']. depelim tt'. exists u; term. depelim H0. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid Arith Wf_nat