bundle

proveit.bundle(expr, bundle_thm, num_levels=2, \*\*defaults_config)

Given a nested OperationOverInstances, derive or equate an equivalent form in which a given number of nested levels is bundled together. Use the given theorem specific to the particular OperationOverInstances.

For example,

orall_{x, y | Q(x, y)} orall_{z | R(z)} P(x, y, z)

can become

orall_{x, y, z | Q(x, y), R(z)} P(x, y, z)

via bundle with num_levels=2.

For example of the form of the theorem required, see proveit.logic.booleans.quantification.bundling or proveit.logic.booleans.quantification.bundling_equality.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.