proposition: Lemma finSucc_opt_Some' (n : nat) (i i' : Fin.t n) : finSucc_opt i = Some i' -> fin_to_nat i' = S (fin_to_nat i).
proof: Proof. revert i'. induction i; cbn; intros. - destruct n; inv H. cbn. reflexivity. - destruct n; cbn in *. destruct_fin i. destruct (finSucc_opt i) as [ i'' | ] eqn:E; inv H. rewrite fin_to_nat_S. rewrite IHi; auto. now rewrite fin_to_nat_S. 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)