proposition: Lemma map_vect_list_length (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) : length (map_vect_list f vs ls) = length ls.
proof: Proof. revert n vs. induction ls as [ | x ls IH]; cbn; intros. - reflexivity. - destruct vs as [ | y n vs]; cbn; f_equal; auto. 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)