proposition: Lemma L : exists f: nat -> B, forall i, R1 (f i) (f (S i)).
proof: Proof. destruct not_acc_ex as [x H1]. destruct (choice _ next_not_acc_R1) as [h H2]. exists (iterate h (exist _ x H1)). induction i; simpl; auto. Qed.
imports: Relations Classical ClassicalChoice