proposition: Theorem phi_of_psi_succ : forall a b1 b2 n, phi a (cons b1 b2 0 (finite (S n))) = if lt_ge_dec a b1 then [a, (cons b1 b2 0 (finite n))] else [a ,(cons b1 b2 0 (finite (S n)))].
proof: Proof. simpl. intros;case (lt_ge_dec a b1). intro; rewrite compare_rw_lt; auto with T2. destruct 1. subst b1; rewrite compare_rw_eq;auto with T2. rewrite compare_rw_gt;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