proposition: Lemma prop_has_fixpoint_when_true : forall P, P -> has_fixpoint P.
proof: Proof. Proof using. intros P a. set (P' := P). set (g1 := id : P' -> P). set (g2 := id : P -> P'). asserts~ Fix: (forall x, g1 (g2 x) = x). clearbody g1 g2. gen g1 g2. rewrite (prop_eq_self_impl_when_true a). subst P'. intros. set (Y := fun f => (fun x => f (g1 x x)) (g2 (fun x => f (g1 x x)))). applys (has_fixpoint_make Y). { intros f. unfold Y at 1. rewrite~ Fix. } Qed.
imports: TLC(LibTactics LibAxioms)