{motive : Lean.Elab.Term.StructInst.FieldView → Sort u} →
  (t : Lean.Elab.Term.StructInst.FieldView) →
    ((ref : Lean.Syntax) →
        (lhs : List Lean.Elab.Term.StructInst.FieldLHS) →
          (val : Lean.Term) → motive { ref := ref, lhs := lhs, val := val }) →
      motive t