proposition: Lemma Nat_iter_S' {A} (f : A -> A) (a : A) n : Nat.iter (S n) f a = f (Nat.iter n f a).
proof: Proof. reflexivity. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString