fact: Record TM : Type := { state : finType; trans : state * (Vector.t (option Σ) n) -> state * (Vector.t ((option Σ) * move) n); start: state; halt : state -> bool }.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List