proposition: Theorem SecondFixedPoint (s : term) : closed s -> exists t, closed t /\ s (enc t) == t.
proof: Proof. intros cls_s. pose (A := lam(s ((ext app) #0 ((ext (enc (X:= term))) #0)))). pose (t := A (ext A)). exists t. split;[subst t A;Lproc|]. symmetry. change (enc t) with (ext t). unfold t. unfold A at 1. redSteps. now Lsimpl. Qed.