Make prettier notation for the
IntroVars constructs. These should resemble their semantics, so that goals containing them are still somewhat readable. It should additionally fix the need to explicitly state the
TT arguments. Also for ReductionStep!
P ∗ [R] ⊲ [M] Q ∗ [S].. but what about variable bindings?
BiAbd & Abd