proposition: Lemma f_not_in_normal_form : forall i, ~ (nf (f (S i))).
proof: Proof. induction i; red; simpl. inversion 1. inversion H3. inversion H9. inversion H9. simpl in IHi. inversion 1. case (lt_irr H3). Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List