proposition: Lemma is_definitional_for_finite_numbers : forall x : Nat, Acc Le x -> forall y : Nat, EqNat x y -> x = y.
proof: Proof. intros x H. apply (Nat_Induction x H). intros. inversion_clear H0. trivial. intros. inversion_clear H1. cut (x0 = m). intros. rewrite H1. trivial. apply H0. assumption. Qed.
imports: Acc_and_Inf