proposition: Fact Natiter_add a b X (f : X -> X) x : Nat.iter (a+b) f x = Nat.iter a f (Nat.iter b f x).
proof: Proof. induction a; simpl; f_equal; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils pos subcode sss) Undecidability.Synthetic(ReducibilityFacts) Undecidability.TM(SBTM pctm_defs)