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 ).