proposition: Lemma fin_to_nat_S (n : nat) (i : Fin.t n) : fin_to_nat (Fin.FS i) = S (fin_to_nat i).
proof: Proof. unfold fin_to_nat. destruct i as [ | n i]. - cbn. reflexivity. - cbn in *. destruct (Fin.to_nat i) as [k ?]. cbn in *. reflexivity. 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)