{Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Γ] →
      (motive : Turing.TM0.Cfg Γ Λ → Sort u_3) →
        (x : Turing.TM0.Cfg Γ Λ) → ((q : Λ) → (T : Turing.Tape Γ) → motive { q := q, Tape := T }) → motive x