proposition: Theorem lt_alpha_psi : forall alpha beta, alpha < [alpha, beta].
proof: Proof. induction alpha. unfold psi;auto with T2. intros. constructor 2. apply lt_le_trans with [alpha1,alpha2];auto with T2. apply lt_le_trans with [ alpha1,alpha2];auto with T2. apply lt_beta_psi. right;constructor 2. apply lt_le_trans with [alpha1,alpha2];auto with T2. apply lt_le_trans with [ alpha1,alpha2];auto with T2. apply lt_beta_psi. right. constructor 2. apply lt_le_trans with [ alpha1,alpha2];auto with T2. apply transitivity with [alpha2, beta];auto with T2. constructor 2. apply lt_beta_cons. apply lt_beta_psi. 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