(motive : List Lean.Elab.Term.StructInst.FieldLHS → Sort u_1) →
  (x : List Lean.Elab.Term.StructInst.FieldLHS) →
    ((first : Lean.Elab.Term.StructInst.FieldLHS) →
        (rest : List Lean.Elab.Term.StructInst.FieldLHS) → motive (first :: rest)) →
      ((x : List Lean.Elab.Term.StructInst.FieldLHS) → motive x) → motive x