Should we show how STS relations are inductive datatypes?

After some internal discussions, it seems we need to settle the question of how to present our STS relations. This is a follow-up to this comment: https://github.com/IntersectMBO/formal-ledger-specifications/issues/663#issuecomment-2633791011

The two main options are:
1. We say that they are relations between the environment, signal and two states that are defined by the natural deduction rules we give in the figure. We do not explain how this is implemented in Agda and hide everything that hints toward the implementation (e.g. `data` and `where` keywords). This would mirror the style of the old PDF specs. It would look something like this:
```agda
_⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type

RTC-base :
Γ ⊢ s ⇀⟦ [] ⟧* s

RTC-ind :
∙ Γ ⊢ s ⇀⟦ sig ⟧ s'
∙ Γ ⊢ s' ⇀⟦ sigs ⟧* s''
─────────────────────────
Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
```
2. We show the definition of the relations in full and explain to a degree what they mean. Note that this means we'd be showing that STS relations are just sum types (which we use in a bunch of places as normal non-dependent sum types). To provide understanding that these are the same, we'd have to explain how to desugar the `∙_`, `_∙_` and `_──────────────────────_` symbols. It would look something like this:
```agda
data _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type where

RTC-base :
Γ ⊢ s ⇀⟦ [] ⟧* s

RTC-ind :
∙ Γ ⊢ s ⇀⟦ sig ⟧ s'
∙ Γ ⊢ s' ⇀⟦ sigs ⟧* s''
─────────────────────────
Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
```
Compare this with a data type we already have:
```agda
data Credential : Type where
KeyHashObj : KeyHash → Credential
ScriptObj : ScriptHash → Credential
```

My personal opinion is that most of the target audience does not care that our relations are datatypes, and showing that they are will mostly lead to confusion and distraction. For somebody consuming the PDF as a piece of documentation, knowing how to work with values of these types is completely irrelevant. There is of course some potential for confusing people familiar with Agda or dependent types in general, but these people can always just have a look at the source code.