# Library Fixpoints

Require Export Encoding.

Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.

Proof.

intros cls_s.

pose (A := lam (s (#0 #0))).

pose (t := A A).

exists t. split; value.

symmetry. cbv. crush.

Qed.

Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (tenc t) == t.

Proof.

intros cls_s.

pose (A := lam(s (App #0 (Q #0)))).

pose (t := A (tenc A)).

exists t. split; value.

symmetry. unfold t, A.

transitivity (s (App (tenc A) (Q (tenc A)))). crush.

rewrite Q_correct, App_correct. reflexivity.

Qed.

Goal exists t, closed t /\ t == (tenc t).

Proof.

destruct (SecondFixedPoint) with ( s := I) as [t [cls_t A]]. value.

exists t.

split; value. symmetry in A. eapply (eqTrans A). crush.

Qed.