proposition: Lemma phi_fix alpha beta : phi alpha beta = beta -> {beta1 : T2 & {beta2 : T2 | beta = [beta1, beta2] /\ alpha t2< beta1}}.
proof: Proof. destruct beta;simpl. discriminate 1. - case n. + case beta3. * case_eq (compare alpha beta1). -- intros H H0; injection H0. intro; absurd (lt beta2 [beta1, beta2]). ++ rewrite H1; apply lt_irr. ++ refine (lt_beta_psi _ _). -- exists beta1, beta2; split;auto with T2. -- intros H H0; injection H0. intro H1; absurd (beta2 t2< [beta1, beta2]). ++ rewrite H1;apply lt_irr. ++ refine (lt_beta_psi _ _). * destruct t;simpl. destruct t;simpl. destruct t;simpl. case (compare alpha beta1). all: try discriminate 1. + discriminate 1. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)