proposition: Lemma compare_rw_eq : forall alpha beta, alpha = beta -> compare alpha beta = Eq.
proof: Proof. intros; generalize (compare_reflect alpha beta). case (compare alpha beta). auto with T2. intro H0;subst beta;case (lt_irr H0). intro H0;subst beta;case (lt_irr H0). 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