Operations on Theorems for forward-reasoning

[brianhuffman]

Currently there's not much you can do in saw-script with a Theorem value: You can print it, and if it's an equation you can add it to a Simpset.

It would be nice to have some additional operations that would enable forward reasoning:

• Rewriting of theorems with a Simpset
• Instantiating universal quantifiers
• Generalizing over symbolic variables
• Modus ponens, i.e. implication elimination
• Symmetry and transitivity of equation theorems

[robdockins]

There are at least experimental versions of many of these operations now. What still needs to be done to close this ticket?