∀ {α : Type} (ea : Computability.FinEncoding α) (x : α),
  (flip bind (Turing.idComputer ea).step)^[1]
      (some (Turing.initList (Turing.idComputer ea) (List.map (Equiv.cast ⋯).invFun (ea.encode x)))) =
    (flip bind (Turing.idComputer ea).step)^[1]
      (some (Turing.initList (Turing.idComputer ea) (List.map (Equiv.cast ⋯).invFun (ea.encode x))))