DEFINITION well_founded()
TYPE =
Π
A:
Set
.(A
→
A
→
Prop
)
→
Prop
BODY =
Show proof