(motive : Lean.Meta.PreprocessResult✝ → Sort u_1) →
  (x : Lean.Meta.PreprocessResult✝) →
    ((type cacheKeyType : Lean.Expr) →
        (kind : Lean.Meta.PreprocessKind✝) → motive { type := type, cacheKeyType := cacheKeyType, kind := kind }) →
      motive x