proposition: Lemma succ_of_cons : forall a b n c, zero< a \/ zero< b -> succ (cons a b n c)= cons a b n (succ c).
proof: Proof. destruct a;destruct b;simpl;auto with T2. destruct 1 as [H|H];inversion H. 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