feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures

It seems most of the time these theorems are not used at all.
They are just polluting the namespace.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>