(motive : Lean.Meta.DefEqCacheKind → Sort u_1) →
  (x : Lean.Meta.DefEqCacheKind) →
    (Unit → motive Lean.Meta.DefEqCacheKind.transient) → (Unit → motive Lean.Meta.DefEqCacheKind.permanent) → motive x