proposition: Theorem subterm_lt : forall alpha beta, subterm alpha beta -> nf beta -> alpha < beta.
proof: Proof. induction 1;auto with T2. intro;apply lt_tail;auto with T2. intro; apply transitivity with t1;auto with T2. eapply IHsubterm1. eapply nf_subterm;eauto with T2. 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