proposition: Lemma map_vect_list_app (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) (x : X) (i : Fin.t n) : fin_to_nat i = length ls -> map_vect_list f vs (ls ++ [x]) = map_vect_list f vs ls ++ [f x vs[@i]].
proof: Proof. revert n vs i. induction ls as [ | x' ls IH]; cbn; intros. - destruct vs. destruct_fin i. enough (i = Fin.F1) as -> by auto. pose proof fin_destruct_S i as [ (i'&->) | ]; cbn in *; auto. rewrite fin_to_nat_S in *. lia. - destruct vs as [ | v n vs]; cbn in *. + destruct_fin i. + f_equal. pose proof fin_destruct_S i as [ (i'&->) | -> ]; cbn in *. * rewrite fin_to_nat_S in *. apply IH. lia. * lia. 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)