proposition: Lemma finSucc_opt_None' (n : nat) (i : Fin.t n) : finSucc_opt i = None -> S (fin_to_nat i) = n.
proof: Proof. induction i; cbn; intros. - destruct n; now inv H. - destruct n. destruct_fin i. destruct (finSucc_opt i) as [ i' | ]; inv H. now rewrite fin_to_nat_S, IHi. 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)