proposition: Theorem lt_beta_psi : forall beta alpha, beta < [alpha, beta].
proof: Proof. induction beta. auto with T2. intros. cut (beta2 < [alpha, (cons beta1 beta2 n beta3)]). intro H. tricho beta1 alpha H0. auto with T2. subst alpha. constructor 3. apply lt_le_trans with [beta1, beta2];auto with T2. case (psi_le_cons beta1 beta2 n beta3). intro. pattern (cons beta1 beta2 n beta3) at 2. rewrite <- H1. unfold psi;constructor 5;auto with T2. unfold psi; constructor 4;auto with T2. assert ([alpha, beta2] < [alpha, (cons beta1 beta2 n beta3)]). constructor 3. apply lt_le_trans with [beta1, beta2]; auto with T2. eapply transitivity;eauto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo