proposition: Lemma Nat_iter_id {A} (a : A) n : Nat.iter n (fun a : A => a) a = a.
proof: Proof. induction n in a |- *; cbn. - reflexivity. - unfold Nat.iter in IHn. now rewrite <- IHn. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString