Library Fixpoints
First Fixed Point Theorem
Theorem
FirstFixedPoint
(
s
:
term
) :
closed
s
→
∃
t
,
closed
t
∧
s
t
==
t
.
Second Fixed Point Theorem
Theorem
SecondFixedPoint
(
s
:
term
) :
closed
s
→
∃
t
,
closed
t
∧
s
(
tenc
t
)
==
t
.
Goal
∃
t
,
closed
t
∧
t
==
(
tenc
t
)
.