{motive : Lean.Elab.Command.Structure.StructFieldViewDefault → Sort u} →
  ((value : Lean.Syntax) → motive (Lean.Elab.Command.Structure.StructFieldViewDefault.optParam value)) →
    ((tactic : Lean.Syntax) → motive (Lean.Elab.Command.Structure.StructFieldViewDefault.autoParam tactic)) →
      (t : Lean.Elab.Command.Structure.StructFieldViewDefault) → motive t