proposition: Lemma nf2_phi0R : forall a b, b < phi0 a -> nf2 b a.
proof: Proof. induction b. constructor. inversion_clear 1. constructor;auto. inversion H0. inversion H0. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List