(motive : List Lean.Elab.Command.Scope → Sort u_1) →
  (x : List Lean.Elab.Command.Scope) →
    (Unit → motive []) →
      ((h : Lean.Elab.Command.Scope) → (t : List Lean.Elab.Command.Scope) → motive (h :: t)) → motive x