proposition: Lemma cycle_not_acc : forall A (R : relation A) (a : A), R a a -> ~Acc R a.
proof: Proof. intros A R a H Acc_a; generalize H; clear H; induction Acc_a as [a Acc_a IH]. intro H; apply (IH a); trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)