proposition: Lemma phi_le_ge : forall alpha beta, nf alpha -> nf beta -> {alpha':T2 & {beta':T2 | phi alpha beta = [alpha' ,beta'] /\ alpha <= alpha' /\ beta' <= beta}}.
proof: Proof. intros a b Va Vb; case (phi_cases' a Vb). destruct 1. case s; intros b1 (b2,(H1,(H2,H3))). rewrite H1 in H3. subst b. exists b1;exists b2;repeat split;auto with T2. exists a;exists b;auto with T2. intros (b1,(b2,(n,(H1,(H2,H3))))). exists a;exists (cons b1 b2 0 (finite n));auto with T2. split;auto with T2. split;auto with T2. subst b;case n;simpl; auto with T2. right;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