proposition: Lemma finMin_opt_Some_val (n : nat) i : finMin_opt n = Some i -> fin_to_nat i = 0.
proof: Proof. destruct n; cbn; intros H; inv H; auto. 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)