∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (motive : Turing.TM1.Cfg Γ Λ σ → Prop)
  (x : Turing.TM1.Cfg Γ Λ σ),
  (∀ (l₁ : Option Λ) (v : σ) (T : Turing.Tape Γ), motive { l := l₁, var := v, Tape := T }) → motive x