proposition: Lemma lt_subterm2 : forall a a' n n' b b', a < a' -> nf (cons a n b) -> nf (cons a' n' b') -> b < cons a' n' b'.
proof: Proof. intros. apply le_lt_trans with (cons a n b). right. apply tail_lt_cons;auto. constructor. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List