{m : Type → Type} →
  {motive : Lean.Meta.Sym.Internal.MonadShareCommon m → Sort u} →
    ((share1 : Lean.Expr → m Lean.Expr) →
        (assertShared : Lean.Expr → m Unit) →
          (isDebugEnabled : m Bool) →
            motive { share1 := share1, assertShared := assertShared, isDebugEnabled := isDebugEnabled }) →
      (t : Lean.Meta.Sym.Internal.MonadShareCommon m) → motive t