(motive : ℕ × Lean.NameMap Lean.Expr × Array (Lean.TSyntax `Lean.Parser.Term.structInstField) → Sort u_1) →
  (x : ℕ × Lean.NameMap Lean.Expr × Array (Lean.TSyntax `Lean.Parser.Term.structInstField)) →
    ((i : ℕ) →
        (fieldValues : Lean.NameMap Lean.Expr) →
          (fields : Array (Lean.TSyntax `Lean.Parser.Term.structInstField)) → motive (i, fieldValues, fields)) →
      motive x