proposition: Lemma mapTape_ext (sig tau : Type) (f g : sig -> tau) (t : tape sig) : (forall a, f a = g a) -> mapTape f t = mapTape g t.
proof: Proof. intros H. destruct t; cbn; auto; simpl_tape; rewrite H; f_equal; eapply map_ext; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM