proposition: Lemma fin_is_1 (n : nat) (i : Fin.t (S (S n))) : fin_to_nat i = 1 -> i = Fin1.
proof: Proof. intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; [|easy]. rewrite fin_to_nat_S in H. inv H. now apply fin_is_0 in H1 as ->. 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)