proposition: Lemma lt_subterm1 : forall a a' n' b', a < a' -> a < cons a' n' b'.
proof: Proof. intros. apply lt_trans with (cons a n' b');auto with T1. apply head_lt_cons. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List