proposition: Lemma finSucc_opt_None (n : nat) (i : Fin.t n) : S (fin_to_nat i) = n -> finSucc_opt i = None.
proof: Proof. induction i; intros; cbn in *. - inv H. reflexivity. - rewrite fin_to_nat_S in *. inv H. spec_assert IHi by assumption. destruct n; cbn. lia. rewrite IHi. 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)