proposition: Lemma nat_2_term_mono : forall n n', (n < n')%nat -> rpo (nat_2_term n) (nat_2_term n').
proof: Proof. induction 1. - simpl; eapply Subterm. + eleft; esplit. + constructor. - cbn; eapply Subterm. + eleft; esplit. + constructor; 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)