{motive : Lean.Meta.GeneralizeTelescope.Entry → Sort u} →
  (t : Lean.Meta.GeneralizeTelescope.Entry) →
    ((expr type : Lean.Expr) → (modified : Bool) → motive { expr := expr, type := type, modified := modified }) →
      motive t