(motive : List (Lean.Ident × Lean.Ident × Option Lean.Name × Bool) → Sort u_1) →
  (x : List (Lean.Ident × Lean.Ident × Option Lean.Name × Bool)) →
    (Unit → motive []) →
      ((a b : Lean.Ident) →
          (recField : Option Lean.Name) →
            (isProof : Bool) →
              (todo : List (Lean.Ident × Lean.Ident × Option Lean.Name × Bool)) →
                motive ((a, b, recField, isProof) :: todo)) →
        motive x