proposition: Lemma mapTape_mapTape (sig tau gamma : Type) (f : sig -> tau) (g : tau -> gamma) (t : tape sig) : mapTape g (mapTape f t) = mapTape (fun x => g (f x)) t.
proof: Proof. destruct t; cbn; auto; try simpl_tape; now rewrite !map_map. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM