Definition. wf_equi
wf R M ↔ ∀A. A ⊆ M → ¬A = ∅ →
∃y. y ∈ A ∧ ¬∃x. x ∈ A ∧ (x, y) ∈ R
A relation R is called well-founded on M, if every
non-empty set A ⊆ M posesses a minimal element y. The corresponding
induction principle is shown by wf_induction_set and wf_induction.