proposition: Theorem lt_alpha_psi : forall alpha beta, alpha t2< [alpha, beta].
proof: Proof. induction alpha. - unfold psi;auto with T2. - intros beta; constructor 2. + apply lt_le_trans with [alpha1,alpha2];auto with T2. + apply lt_le_trans with [ alpha1,alpha2];auto with T2. * apply lt_beta_psi. * right;constructor 2. -- apply lt_le_trans with [alpha1,alpha2];auto with T2. -- apply lt_le_trans with [ alpha1,alpha2];auto with T2. ++ apply lt_beta_psi. ++ right; constructor 2. ** apply lt_le_trans with [ alpha1,alpha2];auto with T2. ** apply lt_trans with [alpha2, beta];auto with T2. constructor 2. apply lt_beta_cons. apply lt_beta_psi. 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)