{motive : Lean.AttributeApplicationTime → Sort u} →
  (t : Lean.AttributeApplicationTime) →
    motive Lean.AttributeApplicationTime.afterTypeChecking →
      motive Lean.AttributeApplicationTime.afterCompilation →
        motive Lean.AttributeApplicationTime.beforeElaboration → motive t