proposition: Lemma succ_nf : forall a, nf a -> nf (succ a).
proof: Proof. induction a. simpl. repeat constructor; auto with arith. simpl. generalize IHa1 ; case a1. simpl;repeat constructor; auto. intros c n0 c0 H H0. apply nf_intro. nf_inv. apply IHa2; nf_inv. apply succ_nf2. eapply nf2_intro; eauto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List