DEFINITION well_founded()
TYPE =
Π
A:
Set
.(A
→
A
→
Prop
)
→
Prop
BODY =
λ
A:
Set
.
λ
R:A
→
A
→
Prop
.
∀
a:A.(
Acc
A R a)