Prove an equivalence between the two ledgers

[WhatisRT]

We have two models right now, one under Ledger and one under Ledger.Conway.Conformance. They differ by some logic being moved from CERTS into UTXO but are otherwise identical. This means that there should be a theorem of the form

Γ L.⊢ s ⇀⦇ tx ,LEDGER⦈ s' ⇔ Γ C.⊢ s ⇀⦇ tx ,LEDGER⦈ s'

except that we need to translate some of the types being involved (otherwise this won't type check). In the end, we need to prove this for CHAIN, but that should be trivial once we have it for LEDGER.

Our current strategy for maintenance is based on this being proven, otherwise these could drift out of sync. So the sooner this is done the better.

See also #512, which will actually make this provable once finished and #525.

Blocked by #512 and it would be a good idea to do #582 first.