proposition: Lemma nf_Wf : well_founded_P _ nf lt.
proof: Proof. unfold well_founded_P. intros. unfold restrict. generalize (Acc_inverse_image _ _ rpo T2_2_term a (well_founded_rpo (T2_2_term a))). intro. eapply Acc_incl with (fun x y : T2 => rpo (T2_2_term x) (T2_2_term y)). red. apply R_inc_rpo. auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo