proposition: Lemma map_vect_list_eq (X Y : Type) (n1 : nat) (f : X -> Y -> X) (vs : Vector.t Y n1) (xs : Vector.t X n1) : map_vect_list f vs (vector_to_list xs) = vector_to_list (Vector.map2 f xs vs).
proof: Proof. revert xs. induction vs as [ | v n1 vs IH]; intros; cbn in *. - revert xs. apply Vector.case0. reflexivity. - apply (Vector.caseS' xs). intros. cbn. f_equal. apply IH. Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)