proposition: Lemma nf_tail_lt_nf : forall b b', b' < b -> nf b' -> forall a n, nf (cons a n b) -> nf (cons a n b').
proof: Proof. induction 1. constructor; eauto with T1. constructor. apply lt_trans with a'; auto. inversion H1; eauto with T1. eauto with T1. assumption. constructor. inversion H1;eauto with T1. eauto with T1. assumption. constructor. inversion H1;eauto with T1. eauto with T1. assumption. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List