proposition: Lemma lt_acc : forall (n : nat) (y : E), f y < n -> Acc R y.
proof: Proof. simple induction n. intros; absurd (f y < 0); auto with arith. intros; apply Acc_intro. intros; apply H. apply lt_le_trans with (m := f y); auto with arith. Qed.
imports: Arith Omega List