protected + nesting

Stream: lean4

[Eric Rodriguez]

wondering whether it's intended that protected doesn't actually protect more than the "innermost" namespace, i.e.:

namespace A.B.C.D.E.F

theorem abcdef : True := by trivial

protected theorem x : True := by trivial
-- all of these work
#check A.B.C.D.E.F.x
#check B.C.D.E.F.x
#check F.x
-- this fails
#check x

[François G. Dorais]

It always worked that way. Do you have a use case where deeper protection is needed?