diff --git a/src/Ledger/Conway/Conformance/Properties.agda b/src/Ledger/Conway/Conformance/Properties.agda
index b5d0cf224..81ae8a04d 100644
--- a/src/Ledger/Conway/Conformance/Properties.agda
+++ b/src/Ledger/Conway/Conformance/Properties.agda
@@ -48,9 +48,6 @@ getRewards = DState.rewards ∘ CertState.dState ∘ LState.certState ∘ getLSt
 allDReps : NewEpochState → DReps
 allDReps = GState.dreps ∘ CertState.gState ∘ LState.certState ∘ getLState
 
-activeDReps : Epoch → NewEpochState → ℙ Credential
-activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (allDReps s))
-
 getGovState : NewEpochState → GovState
 getGovState = LState.govSt ∘ getLState
 
diff --git a/src/Ledger/Conway/Specification/Certs.lagda.md b/src/Ledger/Conway/Specification/Certs.lagda.md
index e3fc393fe..47a3c1393 100644
--- a/src/Ledger/Conway/Specification/Certs.lagda.md
+++ b/src/Ledger/Conway/Specification/Certs.lagda.md
@@ -67,9 +67,6 @@ instance
 CCHotKeys : Type
 CCHotKeys = Credential ⇀ Maybe Credential
 
-DReps : Type
-DReps = Credential ⇀ Epoch
-
 PoolEnv : Type
 PoolEnv = PParams
 
@@ -94,9 +91,6 @@ StakeDelegs = Credential ⇀ KeyHash
 record HasCCHotKeys {a} (A : Type a) : Type a where
   field CCHotKeysOf : A → CCHotKeys
 
-record HasDReps {a} (A : Type a) : Type a where
-  field DRepsOf : A → DReps
-
 record HasPools {a} (A : Type a) : Type a where
   field PoolsOf : A → Pools
 
@@ -113,7 +107,6 @@ record HasStakeDelegs {a} (A : Type a) : Type a where
   field StakeDelegsOf : A -> StakeDelegs
 
 open HasCCHotKeys ⦃...⦄ public
-open HasDReps ⦃...⦄ public
 open HasPools ⦃...⦄ public
 open HasRetiring ⦃...⦄ public
 open HasRewards ⦃...⦄ public
@@ -125,6 +118,7 @@ open HasStakeDelegs ⦃...⦄ public
 
 ## Delegation Definitions
 
+
 ```agda
 data DCert : Type where
   delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
diff --git a/src/Ledger/Conway/Specification/Enact.lagda.md b/src/Ledger/Conway/Specification/Enact.lagda.md
index 476867e3e..2e96dda4d 100644
--- a/src/Ledger/Conway/Specification/Enact.lagda.md
+++ b/src/Ledger/Conway/Specification/Enact.lagda.md
@@ -84,6 +84,9 @@ ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credenti
 ccCreds (just x   , _)  = dom (x .proj₁)
 ccCreds (nothing  , _)  = ∅
 
+ℚof? : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → Maybe ℚ
+ℚof? cc' = proj₂ <$> (proj₁ cc')
+
 getHash : ∀ {a} → NeedsHash a → Maybe GovActionID
 getHash {NoConfidence}        h = just h
 getHash {UpdateCommittee}     h = just h
diff --git a/src/Ledger/Conway/Specification/Epoch.lagda.md b/src/Ledger/Conway/Specification/Epoch.lagda.md
index 79242c380..c9d556d89 100644
--- a/src/Ledger/Conway/Specification/Epoch.lagda.md
+++ b/src/Ledger/Conway/Specification/Epoch.lagda.md
@@ -461,31 +461,21 @@ module VDelegDelegatedStake
   (gState       : GState)
   (dState       : DState)
   where
-```
-<!--
-```agda
-  open UTxOState utxoSt
-  open DState dState
-  open GState gState
-```
--->
-```agda
-  -- active DReps
+
   activeDReps : ℙ Credential
-  activeDReps = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) dreps)
+  activeDReps = dom (DRepsOf gState ∣ currentEpoch ≤Expiry)
 
-  -- active vote delegations
   activeVDelegs : ℙ VDeleg
   activeVDelegs = mapˢ vDelegCredential activeDReps ∪ ❴ vDelegNoConfidence ❵ ∪ ❴ vDelegAbstain ❵
 
   -- compute the stake for a credential
   stakePerCredential : Credential → Coin
-  stakePerCredential c = cbalance (utxo ∣^' λ txout → getStakeCred txout ≡ just c)
+  stakePerCredential c = cbalance ((UTxOOf utxoSt) ∣^' λ txout → getStakeCred txout ≡ just c)
                          + fromMaybe 0 (lookupᵐ? (stakeFromGADeposits govSt utxoSt) c)
                          + fromMaybe 0 (lookupᵐ? (RewardsOf dState) c)
 
   calculate : VDeleg ⇀ Coin
-  calculate = mapFromFun (λ vd → ∑ˢ[ c ← voteDelegs ⁻¹ vd ] (stakePerCredential c))
+  calculate = mapFromFun (λ vd → ∑ˢ[ c ← (VoteDelegsOf dState) ⁻¹ vd ] (stakePerCredential c))
                          activeVDelegs
 ```
 <!--
diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md
index deadffcc5..c21bcc9a6 100644
--- a/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md
+++ b/src/Ledger/Conway/Specification/Epoch/Properties/ExpiredDReps.lagda.md
@@ -197,26 +197,28 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
   castVotes : abdr.castVotes ≡ abdr'.castVotes
   castVotes = refl
 
-  activeDReps : abdr.activeDReps ≡ᵉ abdr'.activeDReps
-  activeDReps with Γ≈Γ'.currentEpoch
-  ... | refl = dom-cong $
-    begin
-      filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps ˢ
-        ≈⟨ filterᵐ-idem {m = Γ.dreps} ⟨
-      filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps) ˢ
-        ≈⟨ filter-cong Γ≈Γ'.dreps ⟩
-      filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps) ˢ
-        ≈⟨ filterᵐ-idem {m = Γ'.dreps} ⟩
-      filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps ˢ
-    ∎
-    where
-      open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
+  opaque
+    unfolding DRepsOf_∣_≤Expiry
+
+    activeDReps-≡ᵉ : abdr.activeDReps ≡ᵉ abdr'.activeDReps
+    activeDReps-≡ᵉ with Γ≈Γ'.currentEpoch
+    ... | refl = dom-cong $
+      begin
+        filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps ˢ
+          ≈⟨ filterᵐ-idem {m = Γ.dreps} ⟨
+        filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ.currentEpoch ≤ e) Γ.dreps) ˢ
+          ≈⟨ filter-cong Γ≈Γ'.dreps ⟩
+        filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) (filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps) ˢ
+          ≈⟨ filterᵐ-idem {m = Γ'.dreps} ⟩
+        filterᵐ (λ (_ , e) → Γ'.currentEpoch ≤ e) Γ'.dreps ˢ
+      ∎
+      where open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
 
   predeterminedDRepVotes : abdr.predeterminedDRepVotes ≡ abdr'.predeterminedDRepVotes
   predeterminedDRepVotes = refl
 
   defaultDRepCredentialVotes : abdr.defaultDRepCredentialVotes ≡ᵐ abdr'.defaultDRepCredentialVotes
-  defaultDRepCredentialVotes = map-≡ᵉ (map-≡ᵉ activeDReps)
+  defaultDRepCredentialVotes = map-≡ᵉ (map-≡ᵉ activeDReps-≡ᵉ)
 
   actualVotes : abdr.actualVotes ≡ᵐ abdr'.actualVotes
   actualVotes = ∪ˡ-cong {m = abdr.castVotes} {m' = abdr.defaultDRepCredentialVotes ∪ˡ abdr.predeterminedDRepVotes}
@@ -251,8 +253,8 @@ module AcceptedByDRep-≈ {Γ Γ' : RatifyEnv} (Γ≈Γ' : RatifyEnv- Γ ≈ Γ'
                             (StakeDistrs-_≈_.stakeDistrVDeleg Γ≈Γ'.stakeDistrs)
                             (dom-cong (coresᵐ-cong {m = abdr.actualVotes} {m' = abdr'.actualVotes} actualVotes ≡ᵉ-isEquivalence.refl)))
     where
-      open import Relation.Binary.Structures _≡ᵉ_
-      module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence
+    open import Relation.Binary.Structures _≡ᵉ_
+    module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence
 
   accepted-→ : abdr.accepted → abdr'.accepted
   accepted-→ x =
@@ -510,22 +512,24 @@ module VDelegDelegatedStake-≈
   module vds  = VDelegDelegatedStake currentEpoch utxoSt govSt gState  dState
   module vds' = VDelegDelegatedStake currentEpoch utxoSt govSt gState' dState
 
-  activeDReps : vds.activeDReps ≡ᵉ vds'.activeDReps
-  activeDReps = dom-cong $
-    begin
-      filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ
-        ≈⟨ filterᵐ-idem {m = gState.dreps} ⟨
-      filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps) ˢ
-        ≈⟨ filter-cong gState≈gState'.dreps ⟩
-      filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps) ˢ
-        ≈⟨ filterᵐ-idem {m = gState'.dreps} ⟩
-      filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps ˢ
-    ∎
-    where
-      open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
+  opaque
+    unfolding DRepsOf_∣_≤Expiry
+    activeDReps-≡ᵉ : vds.activeDReps ≡ᵉ vds'.activeDReps
+    activeDReps-≡ᵉ = dom-cong $
+      begin
+        filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps ˢ
+          ≈⟨ filterᵐ-idem {m = gState.dreps} ⟨
+        filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState.dreps) ˢ
+          ≈⟨ filter-cong gState≈gState'.dreps ⟩
+        filterᵐ (λ (_ , e) → currentEpoch ≤ e) (filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps) ˢ
+          ≈⟨ filterᵐ-idem {m = gState'.dreps} ⟩
+        filterᵐ (λ (_ , e) → currentEpoch ≤ e) gState'.dreps ˢ
+      ∎
+      where
+        open import Relation.Binary.Reasoning.Setoid ≡ᵉ-Setoid
 
   activeVDelegs : vds.activeVDelegs ≡ᵉ vds'.activeVDelegs
-  activeVDelegs = ∪-cong (map-≡ᵉ activeDReps) ≡ᵉ-isEquivalence.refl
+  activeVDelegs = ∪-cong (map-≡ᵉ activeDReps-≡ᵉ) ≡ᵉ-isEquivalence.refl
     where
       open import Relation.Binary.Structures _≡ᵉ_
       module ≡ᵉ-isEquivalence = IsEquivalence ≡ᵉ-isEquivalence
diff --git a/src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md b/src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md
index 22126d511..adcf904b4 100644
--- a/src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md
+++ b/src/Ledger/Conway/Specification/Epoch/Properties/NoPropSameDReps.lagda.md
@@ -11,6 +11,7 @@ module Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps
   (abs : AbstractFunctions txs) (open AbstractFunctions abs)
   where
 
+open import Ledger.Conway.Specification.Certs govStructure
 open import Ledger.Conway.Specification.Epoch txs abs
 open import Ledger.Conway.Specification.Gov txs
 open import Ledger.Prelude
@@ -33,7 +34,7 @@ then the set of `activeDReps`{.AgdaField} of `es`{.AgdaBound} in
 ```agda
 prop≡∅⇒activeDReps-const : Epoch → NewEpochState → Type
 prop≡∅⇒activeDReps-const e es =
-  GovStateOf es ≡ [] → activeDReps e es ≡ᵉ activeDReps (sucᵉ e) es
+  GovStateOf es ≡ [] → dom (DRepsOf es ∣ e ≤Expiry) ≡ᵉ dom (DRepsOf es ∣ (sucᵉ e) ≤Expiry)
 ```
 
 *Proof*. (coming soon)
diff --git a/src/Ledger/Conway/Specification/Gov/Actions.lagda.md b/src/Ledger/Conway/Specification/Gov/Actions.lagda.md
index 4ed29f980..7ac7bfbd3 100644
--- a/src/Ledger/Conway/Specification/Gov/Actions.lagda.md
+++ b/src/Ledger/Conway/Specification/Gov/Actions.lagda.md
@@ -11,15 +11,16 @@ This section defines several concepts and types used to represent governance act
 ```agda
 {-# OPTIONS --safe #-}
 
+open import Ledger.Conway.Specification.Gov.Base
+
+module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where
+
 open import Data.Nat.Properties using (+-0-monoid)
 open import Data.Rational using (ℚ; 0ℚ; 1ℚ)
 
 open import Tactic.Derive.Show
 
 open import Ledger.Prelude as P hiding (yes; no)
-open import Ledger.Conway.Specification.Gov.Base
-
-module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where
 ```
 -->
 
@@ -441,3 +442,27 @@ proposedCC ⟦ UpdateCommittee , (x , _ , _) ⟧ᵍᵃ = dom x
 proposedCC _ = ∅
 ```
 
+```agda
+DReps : Type
+DReps = Credential ⇀ Epoch
+```
+
+<!--
+```agda
+record HasDReps {a} (A : Type a) : Type a where
+  field DRepsOf : A → DReps
+open HasDReps ⦃...⦄ public
+
+opaque
+```
+-->
+
+The following function takes a type `A`{.AgdaDatatype} with an associated set of
+`DReps`{.AgdaDatatype}, and an epoch `e`{.AgdaBound}, and returns the
+`DReps`{.AgdaDatatype} of `A`{.AgdaDatatype} that expire in epoch `e`{.AgdaBound} or
+later.
+
+```agda
+  DRepsOf_∣_≤Expiry : {A : Type} ⦃ _ : HasDReps A ⦄ → A → Epoch → DReps
+  DRepsOf a ∣ e ≤Expiry = filterᵐ (λ (_ , expEpoch) → e ≤ expEpoch) (DRepsOf a)
+```
diff --git a/src/Ledger/Conway/Specification/Properties.lagda.md b/src/Ledger/Conway/Specification/Properties.lagda.md
index 7bd6debf8..3f8d09795 100644
--- a/src/Ledger/Conway/Specification/Properties.lagda.md
+++ b/src/Ledger/Conway/Specification/Properties.lagda.md
@@ -74,16 +74,7 @@ instance
   isGADeposit? {PoolDeposit x} = ⁇ (no λ ())
   isGADeposit? {DRepDeposit x} = ⁇ (no λ ())
   isGADeposit? {GovActionDeposit x} = ⁇ (yes tt)
-```
--->
 
-```agda
-activeDReps : Epoch → NewEpochState → ℙ Credential
-activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (DRepsOf s))
-```
-
-<!--
-```agda
 instance
   _ : IsSet Block Tx
   _ = record { toSet = fromList ∘ Block.ts }
diff --git a/src/Ledger/Conway/Specification/Ratify.lagda.md b/src/Ledger/Conway/Specification/Ratify.lagda.md
index 4bd51ea4f..ad23daf86 100644
--- a/src/Ledger/Conway/Specification/Ratify.lagda.md
+++ b/src/Ledger/Conway/Specification/Ratify.lagda.md
@@ -10,14 +10,15 @@ source_path: src/Ledger/Conway/Specification/Ratify.lagda.md
 
 {-# OPTIONS --safe #-}
 
+open import Ledger.Conway.Specification.Transaction hiding (Vote)
+
+module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where
+
 import Data.Integer as ℤ
 open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
 open import Data.Nat.Properties hiding (_≟_; _≤?_)
 
 open import Ledger.Prelude hiding (_∧_; _∨_; _⊔_) renaming (filterᵐ to filter; ∣_∣ to _↓)
-open import Ledger.Conway.Specification.Transaction hiding (Vote)
-
-module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where
 
 open import Ledger.Conway.Specification.Certs govStructure
 open import Ledger.Conway.Specification.Enact govStructure
@@ -314,8 +315,8 @@ module AcceptedByCC (currentEpoch : Epoch)
 ```
 <!--
 ```agda
-  open EnactState eSt using (cc; pparams)
-  open PParams (proj₁ pparams)
+  open EnactState eSt using (cc)
+  open PParams (PParamsOf eSt)
   open GovActionState gaSt
   open GovVotes votes using (gvCC)
 ```
@@ -345,7 +346,7 @@ module AcceptedByCC (currentEpoch : Epoch)
                        else constMap (dom m) Vote.no
 
   mT : Maybe ℚ
-  mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC
+  mT = threshold (PParamsOf eSt) (ℚof? cc) action CC
 
   t : ℚ
   t = maybe id 0ℚ mT
@@ -402,9 +403,8 @@ module AcceptedByDRep (Γ : RatifyEnv)
 ```
 <!--
 ```agda
-  open EnactState eSt using (cc; pparams)
-  open RatifyEnv Γ using (currentEpoch; dreps; stakeDistrs)
-  open PParams (proj₁ pparams)
+  open EnactState eSt using (cc)
+  open RatifyEnv Γ using (currentEpoch; stakeDistrs)
   open StakeDistrs stakeDistrs
   open GovActionState gaSt
   open GovVotes votes using (gvDRep)
@@ -416,7 +416,7 @@ module AcceptedByDRep (Γ : RatifyEnv)
   castVotes = mapKeys vDelegCredential gvDRep
 
   activeDReps : ℙ Credential
-  activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
+  activeDReps = dom (DRepsOf Γ ∣ currentEpoch ≤Expiry)
 
   predeterminedDRepVotes : VDeleg ⇀ Vote
   predeterminedDRepVotes = case gaType action of λ where
@@ -428,10 +428,10 @@ module AcceptedByDRep (Γ : RatifyEnv)
 
   actualVotes : VDeleg ⇀ Vote
   actualVotes  = castVotes ∪ˡ defaultDRepCredentialVotes
-                             ∪ˡ predeterminedDRepVotes
+                           ∪ˡ predeterminedDRepVotes
 
   t : ℚ
-  t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep)
+  t = maybe id 0ℚ (threshold (PParamsOf eSt) (ℚof? cc) action DRep)
 
   acceptedStake totalStake : Coin
   acceptedStake  = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes ] x
@@ -523,7 +523,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
 
 <!--
 ```agda
-  open EnactState eSt using (cc; pparams)
+  open EnactState eSt using (cc)
   open GovActionState gaSt
   open GovVotes votes using (gvSPO)
 ```
@@ -547,7 +547,7 @@ module AcceptedBySPO (delegatees : VoteDelegs)
   actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools)
 
   t : ℚ
-  t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO)
+  t = maybe id 0ℚ (threshold (PParamsOf eSt) (ℚof? cc) action SPO)
 
   acceptedStake totalStake : Coin
   acceptedStake  = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes ] x