{m : Type → Type} →
  {motive : Lean.Elab.MonadInfoTree m → Sort u} →
    ((getInfoState : m Lean.Elab.InfoState) →
        (modifyInfoState : (Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit) →
          motive { getInfoState := getInfoState, modifyInfoState := modifyInfoState }) →
      (t : Lean.Elab.MonadInfoTree m) → motive t