Prove-It
Prove-It copied to clipboard
Don't reuse an instantiation if simplification directives have changed
trafficstars
Instantiations are stored and reused for efficiency. However, these should sometimes be invalidated when autosimplification is used and simplification directives change.