Move Carlos's new ledger type relations to their respective Properties files

[williamdemeo]

New relation types were originally proposed in the
Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps module in Carlos's PR #941, but they seem useful and general enough to factor them out and put under the Properties submodule of the modules where the types are defined.

For example,

-- | Epoch indexed relation.
-- Two DReps (Map Credential Epoch) are related iff: Non-expired DReps are the same.
DReps-[_]_≈_ : Epoch → B.Rel DReps 0ℓ
DReps-[_]_≈_ e dreps₁ dreps₂
  = filterᵐ (λ (c , e') → e ≤ e') dreps₁ ≡ᵐ filterᵐ (λ (c , e') → e ≤ e') dreps₂

could be defined in the main Ledger/Conway/Specification/Certs/Properties.lagda.md file (rather than inside a special properties module under Certs/Properties/, because it's essentially a binary relation on one of the types defined in Certs).

Then we could also prove that, for a given epoch e, DReps-[ e ]_≈_ is an equivalence relation on DReps.

Next,

record RatifyEnv-_≈_ (Γ Γ' : RatifyEnv) : Type where
  module Γ  = RatifyEnv Γ
  module Γ' = RatifyEnv Γ'

  field
    stakeDistrs   : StakeDistrs- Γ.stakeDistrs ≈ Γ'.stakeDistrs
    currentEpoch  : Γ.currentEpoch ≡ Γ'.currentEpoch
    dreps         : DReps-[ Γ.currentEpoch ] (DRepsOf Γ) ≈ (DRepsOf Γ')
    ccHotKeys     : Γ.ccHotKeys ≡ Γ'.ccHotKeys
    treasury      : Γ.treasury ≡ Γ'.treasury
    pools         : Γ.pools ≡ Γ'.pools
    delegatees    : Γ.delegatees ≡ Γ'.delegatee

could be defined in Ledger/Conway/Specification/Ratify/Properties.lagda.md and we could prove it's an equivalence relation on RatifyEnvs.

We should also move types like the following into Ratify.Properties:

  cong : ∀ (rSt≡rSt' : rSt ≡ rSt') {rSt'' rSt'''}
       → Γ  ⊢ rSt  ⇀⦇ a ,RATIFY⦈ rSt''
       → Γ' ⊢ rSt' ⇀⦇ a ,RATIFY⦈ rSt'''
       → rSt'' ≡ rSt'''

(This could be renamed to RATIFY-deterministic.)