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