{motive : Lean.Elab.DefViewElabHeader → Sort u} →
  (t : Lean.Elab.DefViewElabHeader) →
    ((toDefView : Lean.Elab.DefView) →
        (toDefViewElabHeaderData : Lean.Elab.DefViewElabHeaderData) →
          (tacSnap? : Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot)) →
            (bodySnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))) →
              motive
                { toDefView := toDefView, toDefViewElabHeaderData := toDefViewElabHeaderData, tacSnap? := tacSnap?,
                  bodySnap? := bodySnap? }) →
      motive t