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

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,

```agda
-- | 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,

```agda
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 `RatifyEnv`s.

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

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

(This could be renamed to `RATIFY-deterministic`.)