proposition: Lemma phi_fix : forall alpha beta, phi alpha beta = beta -> {beta1 : T2 & {beta2 : T2 | beta = [beta1, beta2] /\ alpha < beta1}}.
proof: Proof. destruct beta;simpl. discriminate 1. case n. case beta3. caseEq (compare alpha beta1). intros. injection H0. intro; absurd (lt beta2 [beta1, beta2]). rewrite H1; apply lt_irr. refine (lt_beta_psi _ _). exists beta1. exists beta2; split;auto with T2. intros. injection H0. intro; absurd (beta2 < [beta1, beta2]). rewrite H1;apply lt_irr. refine (lt_beta_psi _ _). destruct t;simpl. destruct t;simpl. destruct t;simpl. case (compare alpha beta1). discriminate 1. discriminate 1. discriminate 1. discriminate 1. discriminate 1. discriminate 1. discriminate 1. 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