Value-TokenAlgebra cannot be instantiated

This issue addresses problems encountered when trying to create a `TokenAlgebra` using `Value-TokenAlgebra ` found in `TokenAlgebra/ValueSet.lagda`. It is not currently possible to instantiate a TokenAlgebra using this library. This is needed in order to implement NFT's in concrete examples.

**Blocking**

1. Concrete implementation of contracts that have NFT's
2. Implementation of example's using structured contracts as they require NFT's

**Issue**

The first problem is that decidable equality is needed to be provided for total maps: `DecEq (TotalMap AssetId ℕ)`. This is not possible to construct.

If as a temporary solution it is postulated that setoid equality is needed instead of DecEq:

e.g.
```
postulate
setoidIsEq : (n m : TotalMap AssetId ℕ) → Dec ((TotalMap.rel n) ≡ᵉ (TotalMap.rel m)) → Dec (n ≡ m)
```

Then it is possible to define:

```
setoidEqualityIsDecidable : ∀ (n m : TotalMap AssetId ℕ) → Dec ((TotalMap.rel n) ≡ᵉ (TotalMap.rel m))
This allowed me to define: DecEq (TotalMap AssetId ℕ).
```

Assuming this issue is solved, a TokenAlgebra can be constructed with Value-TokenAlgebra by passing in 6 arguments :
1. `ℙ AssetId`: A set of AssetId’s
2. `isMaximal assetIds`: A proof that the set of AssetId’s isMaximal
3. `(Dec-lookup≤ : ∀ {u v : AssetId ⇒ ℕ}
→ (∀ {a p q} → lookup u (a , p) ≤ lookup v (a , q)) ⁇)`
4. `PolicyId` : A policy id for the TokenAlgebra
5. `AssetName` : The asset name for the TokenAlgebra.
6. `TotalMap AssetId Quantity → ℕ` : A size function for the TotalMap

For the purpose of running traces on the ledger implementation, I think it is currently possible to define 1,4,5,6 with 6 being a dummy implementation. It is not possible to construct 2 (isMaximal assetIds). I have not tried with 3 so am unaware how difficult this would be.

The `setoidIsEq` postulate may be discharged once we address: Issue #151

**Example**

An example showcasing the above issues can be found in the `value-nft` branch in: (https://github.com/IntersectMBO/formal-ledger-specifications/blob/alasdair/value-nft/src/ScriptVerification/LedgerImplementation.agda ) (Note this is example is far behind master)