{m : Type → Type} →
  {motive : Lean.Compiler.LCNF.MonadScope m → Sort u} →
    ((getScope : m Lean.Compiler.LCNF.Scope) →
        (withScope : {α : Type} → (Lean.Compiler.LCNF.Scope → Lean.Compiler.LCNF.Scope) → m α → m α) →
          motive { getScope := getScope, withScope := withScope }) →
      (t : Lean.Compiler.LCNF.MonadScope m) → motive t