proposition: Theorem lt_beta_psi : forall beta alpha, beta t2< [alpha, beta].
proof: Proof. induction beta. - auto with T2. - intro alpha; assert (H : beta2 t2< [alpha, (gcons beta1 beta2 n beta3)]). { assert ([alpha, beta2] t2< [alpha, (gcons beta1 beta2 n beta3)]). { constructor 3. apply lt_le_trans with [beta1, beta2]; auto with T2. } eapply lt_trans; eauto with T2. } tricho beta1 alpha H0; auto with T2. + subst alpha; constructor 3. apply lt_le_trans with [beta1, beta2];auto with T2. + case (psi_le_cons beta1 beta2 n beta3). * intro; pattern (gcons beta1 beta2 n beta3) at 2; rewrite <- H1. unfold psi; constructor 5; auto with T2. * unfold psi; constructor 4; auto with T2. 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)