import Lean

section
open Lean
open Meta -- ok
end

section
open Lean hiding AttributeImplCore
open Meta -- ok
end