proposition: Theorem le_b_phi_ab : forall a b, nf a -> nf b -> le b (phi a b).
proof: Proof. intros a b Ha Hb; case (phi_cases a Hb). destruct 1. rewrite e;left;auto with T2. rewrite e;right; auto with T2. intro x; case x;intros b' (e,(i,i')). subst b. rewrite i. apply lt_succ_le;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