definition acc_nat: (nat → Prop) → nat →Prop ≝
λP:nat→Prop. λn. ∀m. m ≤ n → P m.
theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
unfold acc_nat; intros 4; elim n names 0; clear n;
definition acc_nat: (nat → Prop) → nat →Prop ≝
λP:nat→Prop. λn. ∀m. m ≤ n → P m.
theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
unfold acc_nat; intros 4; elim n names 0; clear n;