proposition: Fact Natiter_fixpoint n X (f : X -> X) x : f x = x -> Nat.iter n f x = x.
proof: Proof. intros H. induction n as [ | n IHn ]; simpl; auto. rewrite IHn; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)