[LTL] Add ops that allow for all of SVA to be modeled with LTL

[dobios]

This PR adds the ops that were missing to allow us to basically model all of SVA with LTL. This is justified in this design doc and this SVA summary doc.