{motive : Lean.Language.Lean.HeaderProcessedState → Sort u} →
  ((cmdState : Lean.Elab.Command.State) →
      (firstCmdSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
        motive { cmdState := cmdState, firstCmdSnap := firstCmdSnap }) →
    (t : Lean.Language.Lean.HeaderProcessedState) → motive t