proposition: Lemma WF_def {A : Type'} : (@WF A) = (fun _6923 : A -> A -> Prop => forall P : A -> Prop, (exists x : A, P x) -> exists x : A, (P x) /\ (forall y : A, (_6923 y x) -> ~ (P y))).
proof: Proof. exact (eq_refl (@WF A)). Qed.
imports: coq theory_hol types