Entry	Value
Package Name	relation-well-founded-def
Count	1
Theorems	WF : !r. WF r <=> (!p. (?x. p x) ==> (?x. p x /\ (!y. r y x ==> ~p y)))

Back to main package page