Kleene algebra for STS relations

I still support the idea of having explicit constructs from Kleene algebra (*, +, ;, ε, maybe also ∪ for choice to have the full regex) to express this; e.g. for CERTS:
```agda
_⊢_⇀⦇_,CERTS⦈_ = (_⊢_⇀⦇_,CERT⦈_ ⋆) ⨾ _⊢_⇀⦇_,CERTBASE⦈_
```

I think the PDF will look much nicer too and more understandable to people with the relevant background knowledge.

Please create a new issue for that if you agree in general.

_Originally posted by @omelkonian in https://github.com/input-output-hk/formal-ledger-specifications/pull/272#pullrequestreview-1720556377_