If the base cipher `se` is correct, then `etmAEAD se prf` is correct.

The proof is straightforward: the tag comparison
`prf.eval km (ad, c) == prf.eval km (ad, c)` is trivially `true`, so
`decrypt` always reaches the `se.decrypt` branch, which recovers the
plaintext by `hse`. 

**EtM one-time IND-CCA security** (NRS14 Theorem 1 for A5, adapted).

The one-time IND-CCA distinguishing advantage of `etmAEAD se prf` is bounded
by the PRF advantage, the tag-guessing probability per decryption query, and
the IND$-CPA advantage:

  `Adv^{ot-cca-ror}_{EtM}(A) ≤ Adv^{prf}(B) + q_d/|T| + Adv^{ind$}(D)`

where `B = prfReduction se adv` and `D = encReduction se adv` are explicit
reductions (skeleton instantiations), and `q_d` upper-bounds the adversary's
number of decryption queries (tied to `adv` via `decryptQueryBound`, i.e.
`IsQueryBoundP` on the decrypt-oracle index).


The `NeverFail prf.keygen` instance (i.e. `Pr[⊥ | prf.keygen] = 0`) is the explicit form
of a losslessness property NRS14 has implicitly: there keys are sampled from a set, so keygen
cannot fail. Our `prf.keygen : ProbComp K_m` lives in a more permissive, partiality-aware
type, so we state it. It is satisfied by every standard PRF (whose key is a uniform sample
`$ᵗ K_m`), so it doesn't rule out any construction of interest.
NRS14 Figure 9 bound: `Adv^nAE ≤ Adv^prf_F(B) + Adv^ivE_E(D₁) + q_d/2^τ`.
Our one-time adaptation: `Adv^ivE → Adv^{ind$-cpa}`, `2^τ → |T|`.