proposition: Lemma lt_inc_rpo_0 : forall n, forall o' o, (T2_size o + T2_size o' <= n)%nat-> o t2< o' -> nf o -> nf o' -> rpo (T2_2_term o) (T2_2_term o').
proof: Proof. induction n. - destruct o;destruct o'. + inversion 2. + cbn; inversion 1. + inversion 2. + cbn; inversion 1. - destruct o'. + inversion 2. + destruct o. * intros; case (cons_rw o'1 o'2 n0 o'3). intros (H'1,(H'2,H'3)); rewrite H'3. simpl;apply Top_gt. simpl;auto with T2. destruct 1. intro H3;rewrite H3. simpl;apply Top_gt. simpl;auto with T2. destruct 1. * intros; case (Compat815.le_lt_or_eq _ _ H). -- intros;apply IHn;auto with arith T2. -- intros; eapply lt_rpo_cons_cons;eauto 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)