instantiation of theorems having with_wrap options

[wdcraft01]

Some axioms and theorems are crafted with built-in with_wrap options, for both aesthetic and practical reasons. Sometimes the wrapping makes the resulting latex-formatted expression easier to read and understand; sometimes the wrapping helps the resulting expression fit better into the notebook space. The wrapping format, however, is often not as aesthetically pleasing, desirable, or necessary when that same axiom or theorem is instantiated, but the wrapping format is automatically preserved in the instantiated form.

For example, consider the exists_not_eq_not_forall theorem,

which is crafted with the with_wrap_after_operator() option, in part to fit better in the width of a typical notebook:

.

When instantiated, the general theorem can reduce considerably in size and complexity but retain a then-unnecessary wrapped format, like this:

There is nothing functionally problematic or wrong about such a result, but it could be nice to have some convenient option to change the wrapping format in the resulting instantiation. Some possible approaches include:

• making the default behavior to remove such wrapping options in any resulting instantiations;
• providing a user with the ability to set up some set of personal default styles that direct the style of instantiation results;
• utilizing defaults_config to define and provide one or more keyword arguments to allow a user to specify how any wrap options in a theorem will apply in an instantiation result, perhaps something like use_orig_style or maintain_orig_wrapping which could be set to True or False (perhaps having a default setting of True?).

During brief discussion on Fri 8/22/25, @wwitzel thought the defaults_config approach seemed the most promising.