proposition: Lemma psi_le_cons : forall alpha beta n gamma, [alpha, beta] <= cons alpha beta n gamma.
proof: Proof. intros;case n; auto with arith T2. case gamma;auto with arith 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