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