proposition: Theorem wf_classic_wf {A} (R: relation A) : well_founded R -> classic_wf R.
proof: Proof. intros HR [s Hs]. assert (forall x:A, ~ exists i, s i = x). { apply (well_founded_induction HR). intros x Hx [i Hi]. subst x; specialize (Hs i). specialize (Hx _ Hs). apply Hx ; now exists (S i). } apply (H (s 0)); now exists 0. Qed.
imports: Relations