proposition: Theorem FirstFixedPoint (s : term) : closed s -> exists t, closed t /\ s t == t.
proof: Proof. intros cls_s. pose (A := lam (s (#0 #0))). pose (t := A A). exists t. split;[subst t A;Lproc|]. symmetry. cbv. now redStep. Qed.