Test ledger/tx property

Splitting of lemma 3 from input-output-hk/ouroboros-network#1765:
```
applyLedgerBlock cfg blk st
== repeatedlyM (applyTx cfg) (extractTxs blk)
(applyChainTick cfg (blockSlot blk) st)
```
Note that this lemma isn't quite true. For example, in Byron, endorsements come from the protocol version in the header, and aren't an explicit transaction. We should generalise the lemma.

Note that in `cardano-ledger`, they're already checking a similar lemma for Byron.

Note the [following comment](https://github.com/input-output-hk/ouroboros-network/pull/1775#issuecomment-597123263):
> Lemma 3 is harder to check, because of https://github.com/input-output-hk/ouroboros-network/issues/1765#issuecomment-597006390, but also because we suddenly have `ApplyTx blk` and `HasTxs blk` constraints on `applyExtLedger`, which are rather annoying. Adding them as superclasses of `LedgerSupportsProtocol` is convenient, but annoying in `ouroboros-consensus-byron`, because the instances are defined in separate modules. Moreover, `DualByronBlock` doesn't support `HasTxs`, so that's a no go :slightly_frowning_face:.