{m : Type → Type} →
  {motive : Lean.MonadMCtx m → Sort u} →
    (t : Lean.MonadMCtx m) →
      ((getMCtx : m Lean.MetavarContext) →
          (modifyMCtx : (Lean.MetavarContext → Lean.MetavarContext) → m Unit) →
            motive { getMCtx := getMCtx, modifyMCtx := modifyMCtx }) →
        motive t