proposition: Theorem wf_WO : well_founded le_WO.
proof: Proof. unfold well_founded; intro. apply Acc_intro. induction a as [a f IH]. intros y Hle. apply le_WO_inv in Hle. destruct Hle as [a' [g [v [Hy Hsup]]]], Hy. assert (Heq : eq_dep _ (fun a => B a -> WO) a' g a f) by (inversion Hsup;reflexivity). clear Hsup;destruct Heq. apply Acc_intro. apply IH. Qed.
imports: EqdepFacts