proposition: Lemma phi_of_psi_plus_finite : forall a b1 b2 n, a < b1 -> phi a (cons b1 b2 0 (finite n)) < [a ,(cons b1 b2 0 (finite n))].
proof: Proof. simpl. intros until n;case n. simpl. intro H;rewrite (compare_rw_lt H);auto with T2. simpl. intros n0 H;rewrite (compare_rw_lt H). case n0;simpl; auto 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