diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda
index 64b68a316..8d24842be 100644
--- a/src/Ledger/Conway/Conformance/Gov.agda
+++ b/src/Ledger/Conway/Conformance/Gov.agda
@@ -3,16 +3,16 @@
 open import Ledger.Types.GovStructure
 open import Ledger.Transaction using (TransactionStructure)
 
-module Ledger.Conway.Conformance.Gov (txs : _) (open TransactionStructure txs using (govStructure)) where
-open GovStructure govStructure hiding (epoch)
+module Ledger.Conway.Conformance.Gov (txs : _) (open TransactionStructure txs hiding (epoch)) where
 
 open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)
 
 open import Axiom.Set.Properties th using (∃-sublist-⇔)
 
-open import Ledger.GovernanceActions govStructure hiding (yes; no)
+open import Ledger.GovernanceActions govStructure using (Vote)
 open import Ledger.Enact govStructure
 open import Ledger.Conway.Conformance.Ratify txs hiding (vote)
+open import Ledger.Conway.Conformance.Certs govStructure
 
 open import Data.List.Ext using (subpermutations; sublists)
 open import Data.List.Ext.Properties2
@@ -32,8 +32,7 @@ GovState : Type
 GovState = List (GovActionID × GovActionState)
 
 record GovEnv : Type where
-
-  constructor ⟦_,_,_,_,_⟧ᵍ
+  constructor ⟦_,_,_,_,_,_⟧ᵍ
   field
 
     txid        : TxId
@@ -41,12 +40,7 @@ record GovEnv : Type where
     pparams     : PParams
     ppolicy     : Maybe ScriptHash
     enactState  : EnactState
-
-data
-
-  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
-
-_⊢_⇀⦇_,GOV⦈_     : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
+    certState   : CertState
 
 private variable
   Γ : GovEnv
@@ -62,6 +56,9 @@ private variable
   k : ℕ
   p : Maybe ScriptHash
 
+open GState
+open PState
+
 govActionPriority : GovAction → ℕ
 govActionPriority NoConfidence             = 0
 govActionPriority (UpdateCommittee _ _ _)  = 1
@@ -74,13 +71,13 @@ govActionPriority Info                     = 6
 _∼_ : ℕ → ℕ → Type
 n ∼ m = (n ≡ m) ⊎ (n ≡ 0 × m ≡ 1) ⊎ (n ≡ 1 × m ≡ 0)
 
-_≈_ : GovAction → GovAction → Type
-a ≈ a' = (govActionPriority a) ∼ (govActionPriority a')
+_≈ᵍ_ : GovAction → GovAction → Type
+a ≈ᵍ a' = (govActionPriority a) ∼ (govActionPriority a')
 
 _∼?_ : (n m : ℕ) → Dec (n ∼ m)
 n ∼? m = n ≟ m ⊎-dec (n ≟ 0 ×-dec m ≟ 1) ⊎-dec (n ≟ 1 ×-dec m ≟ 0)
 
-_≈?_ : (a a' : GovAction) → Dec (a ≈ a')
+_≈?_ : (a a' : GovAction) → Dec (a ≈ᵍ a')
 a ≈? a' = (govActionPriority a) ∼? (govActionPriority a')
 
 
@@ -91,11 +88,6 @@ insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
      then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
      else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
 
-addVote : GovState → GovActionID → Voter → Vote → GovState
-addVote s aid voter v = map modifyVotes s
-  where modifyVotes = λ (gid , s') → gid , record s'
-          { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
-
 mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
                  → GovActionID × GovActionState
 mkGovStatePair e aid addr a prev = (aid , record
@@ -106,11 +98,29 @@ addAction : GovState
           → GovState
 addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)
 
-validHFAction : GovProposal → GovState → EnactState → Type
-validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
-  (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
-  ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
-validHFAction _ _ _ = ⊤
+opaque
+  addVote : GovState → GovActionID → Voter → Vote → GovState
+  addVote s aid voter v = map modifyVotes s
+    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
+          modifyVotes = λ (gid , s') → gid , record s'
+            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
+
+  isRegistered : GovEnv → Voter → Type
+  isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where
+    CC    → just c ∈ range (gState .ccHotKeys)
+    DRep  → c ∈ dom (gState .dreps)
+    SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
+
+  validHFAction : GovProposal → GovState → EnactState → Type
+  validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
+    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
+    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
+  validHFAction _ _ _ = ⊤
+
+data
+  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
+
+_⊢_⇀⦇_,GOV⦈_   : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
 
 -- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs.
 getAidPairsList : GovState → List (GovActionID × GovActionID)
@@ -147,7 +157,7 @@ hasParentE e aid a = case getHashES e a of
 hasParent : EnactState → GovState → (a : GovAction) → NeedsHash a → Type
 hasParent e s a aid with getHash aid
 ... | just aid' = hasParentE e aid' a
-                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ a) s
+                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ᵍ a) s
 ... | nothing = ⊤
 
 open Equivalence
@@ -236,6 +246,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
     in
     ∙ (aid , ast) ∈ fromList s
     ∙ canVote pparams (action ast) (proj₁ voter)
+    ∙ isRegistered Γ voter
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
 
diff --git a/src/Ledger/Conway/Conformance/Gov/Properties.agda b/src/Ledger/Conway/Conformance/Gov/Properties.agda
index 1b1665266..00ad0c73e 100644
--- a/src/Ledger/Conway/Conformance/Gov/Properties.agda
+++ b/src/Ledger/Conway/Conformance/Gov/Properties.agda
@@ -75,6 +75,9 @@ private
   hasPrev record { action = (TreasuryWdrl _) }        v = no λ ()
   hasPrev record { action = Info }                    v = no λ ()
 
+opaque
+  unfolding validHFAction isRegistered
+
   instance
     validHFAction? : ∀ {p s e} → validHFAction p s e ⁇
     validHFAction? {record { action = NoConfidence }} = Dec-⊤
@@ -93,6 +96,11 @@ private
     validHFAction? {record { action = TreasuryWdrl _ }} = Dec-⊤
     validHFAction? {record { action = Info }} = Dec-⊤
 
+  isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
+  isRegistered? _ (CC   , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (DRep , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (SPO  , _) = ¿ _ ∈ _ ¿
+
 instance
   Computational-GOV' : Computational _⊢_⇀⦇_,GOV'⦈_ String
   Computational-GOV' = record {Go} where
@@ -103,15 +111,18 @@ instance
       module GoVote sig where
         open GovVote sig
 
-        computeProof = case lookupActionId pparams (proj₁ voter) gid s of λ where
-            (yes p) → case Any↔ .from p of λ where
-              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV))
-            (no ¬p)  → failure (genErrors ¬p)
+        computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
+            (yes p , yes p') → case Any↔ .from p of λ where
+              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
+            (yes _ , no ¬p) → failure (genErrors ¬p)
+            (no ¬p , _)     → failure (genErrors ¬p)
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (GOV-Vote (mem , cV)) with lookupActionId pparams (proj₁ voter) gid s
-        ... | no ¬p = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
-        ... | yes p with Any↔ .from p
+        completeness s' (GOV-Vote (mem , cV , reg))
+          with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
+        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
+        ... | yes _ | no ¬p = ⊥-elim $ ¬p reg
+        ... | yes p | yes p' with Any↔ .from p
         ... | (_ , mem , refl , cV) = refl
 
       module GoProp prop where
diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda
index 57a9e2599..5016dc0ff 100644
--- a/src/Ledger/Conway/Conformance/Ledger.agda
+++ b/src/Ledger/Conway/Conformance/Ledger.agda
@@ -19,6 +19,8 @@ open import Ledger.Conway.Conformance.Utxow txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 
 open Tx
+open GState
+open GovActionState
 
 record LEnv : Type where
 
@@ -44,6 +46,17 @@ txgov : TxBody → List (GovVote ⊎ GovProposal)
 txgov txb = map inj₂ txprop ++ map inj₁ txvote
   where open TxBody txb
 
+isUnregisteredDRep : CertState → Voter → Type
+isUnregisteredDRep ⟦ _ , _ , gState ⟧ᶜˢ (r , c) = r ≡ DRep × c ∉ dom (gState .dreps)
+
+removeOrphanDRepVotes : CertState → GovActionState → GovActionState
+removeOrphanDRepVotes certState gas = record gas { votes = votes′ }
+  where
+    votes′ = filterKeys (¬_ ∘ isUnregisteredDRep certState) (votes gas)
+
+_|ᵒ_ : GovState → CertState → GovState
+govSt |ᵒ certState = L.map (map₂ (removeOrphanDRepVotes certState)) govSt
+
 private variable
   Γ : LEnv
   s s' s'' : LState
@@ -70,7 +83,7 @@ data
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     ∙  ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧ˡ
 
diff --git a/src/Ledger/Conway/Conformance/Ledger/Properties.agda b/src/Ledger/Conway/Conformance/Ledger/Properties.agda
index 2baadae49..978a08d7e 100644
--- a/src/Ledger/Conway/Conformance/Ledger/Properties.agda
+++ b/src/Ledger/Conway/Conformance/Ledger/Properties.agda
@@ -64,14 +64,15 @@ instance
       where
       utxoΓ = UTxOEnv ∋ record { LEnv Γ }
       certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ
-      govΓ  = GovEnv  ∋ ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ
+      govΓ : CertState → GovEnv
+      govΓ = ⟦ txid , epoch slot , pparams , ppolicy , enactState ,_⟧ᵍ
 
       computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')
       computeProof = case isValid ≟ true of λ where
         (yes p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
           (certSt' , certStep) ← computeCerts certΓ certSt txcerts
-          (govSt'  , govStep)  ← computeGov   govΓ  govSt  (txgov txb)
+          (govSt'  , govStep)  ← computeGov (govΓ certSt') (govSt |ᵒ certSt') (txgov txb)
           success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
         (no ¬p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
@@ -86,7 +87,7 @@ instance
       ... | success (utxoSt' , _) | refl
         with computeCerts certΓ certSt txcerts | complete _ _ _ _ certStep
       ... | success (certSt' , _) | refl
-        with computeGov govΓ govSt (txgov txb) | complete govΓ _ _ _ govStep
+        with computeGov (govΓ certSt') (govSt |ᵒ certSt') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certSt') _ _ _ govStep
       ... | success (govSt' , _) | refl = refl
       completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
         with isValid ≟ true
@@ -97,337 +98,3 @@ instance
 
 Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String
 Computational-LEDGERS = it
-
-instance
-  HasCoin-LState : HasCoin LState
-  HasCoin-LState .getCoin s = getCoin (LState.utxoSt s)
-
--- ** Proof that LEDGER preserves values.
-
-module _ where
-
-  private variable
-    tx : Tx
-    Γ : LEnv
-    s s' : LState
-    l : List Tx
-
-  FreshTx : Tx → LState → Type
-  FreshTx tx ls = tx .body .txid ∉ mapˢ proj₁ (dom (ls .utxoSt .utxo))
-    where open Tx; open TxBody; open UTxOState; open LState
-
-  data FreshTxs : LEnv → LState → List Tx → Type where
-    []-Fresh : FreshTxs Γ s []
-    ∷-Fresh  : FreshTx tx s → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → FreshTxs Γ s' l
-              → FreshTxs Γ s (tx ∷ l)
-
--- ** Proof that the set equality `govDepsMatch` (below) is a LEDGER invariant.
-
--- Mapping a list of `GovActionID × GovActionState`s to a list of
--- `DepositPurpose`s is so common, we give it a name `dpMap`;
--- it's equivalent to `map (λ (id , _) → GovActionDeposit id)`.
-dpMap : GovState → List DepositPurpose
-dpMap = map (GovActionDeposit ∘ proj₁)
-
-isGADeposit : DepositPurpose → Type
-isGADeposit dp = isGADepositᵇ dp ≡ true
-  where
-  isGADepositᵇ : DepositPurpose → Bool
-  isGADepositᵇ (GovActionDeposit _) = true
-  isGADepositᵇ _                    = false
-
-govDepsMatch : LState → Type
-govDepsMatch ⟦ utxoSt , govSt , _ ⟧ˡ =
-  filterˢ isGADeposit (dom (UTxOState.deposits utxoSt)) ≡ᵉ fromList (dpMap govSt)
-
-module _  -- ASSUMPTIONS (TODO: eliminate/prove these) --
-  {- 1 -} {filterCD : ∀ pp c → filterˢ isGADeposit (dom (certDeposit c pp)) ≡ᵉ ∅}
-  {- 2 -} {filterCR : (c : DCert) {deps : DepositPurpose ⇀ Coin}
-                      → filterˢ isGADeposit (dom ( deps ∣ certRefund c ᶜ ˢ )) ≡ᵉ filterˢ isGADeposit (dom (deps ˢ))}
-  where
-  module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {DepositPurpose})
-  pattern UTXOW-UTXOS x = UTXOW⇒UTXO (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x)
-
-  filterGA : ∀ txid n → filterˢ isGADeposit ❴ GovActionDeposit (txid , n) ❵ ≡ᵉ ❴ GovActionDeposit (txid , n) ❵
-  proj₁ (filterGA txid n) {a} x = (proj₂ (from ∈-filter x)) where open Equivalence
-  proj₂ (filterGA txid n) {a} x = to ∈-filter (ξ (from ∈-singleton x) , x)
-    where
-    open Equivalence
-    ξ : a ≡ GovActionDeposit (txid , n) → isGADeposit a
-    ξ refl = refl
-
-  module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
-    open Tx tx renaming (body to txb); open TxBody txb
-    open LEnv Γ renaming (pparams to pp)
-    open PParams pp using (govActionDeposit)
-
-    -- initial utxo deposits
-    utxoDeps : DepositPurpose ⇀ Coin
-    utxoDeps = UTxOState.deposits (LState.utxoSt s)
-
-    -- GovState definitions and lemmas --
-    mkAction : GovProposal → ℕ → GovActionID × GovActionState
-    mkAction p n = let open GovProposal p in
-      mkGovStatePair
-        (PParams.govActionLifetime pp +ᵉ (epoch slot))
-        (txid , n) returnAddr action prevAction
-
-    -- update GovState with a proposal
-    propUpdate : GovState → GovProposal → ℕ → GovState
-    propUpdate s p n = insertGovAction s (mkAction p n)
-
-    -- update GovState with a vote
-    voteUpdate : GovState → GovVote → GovState
-    voteUpdate s v = addVote s gid voter vote
-      where open GovVote v
-
-    -- update GovState with a list of votes and proposals
-    updateGovStates : List (GovVote ⊎ GovProposal) → ℕ → GovState → GovState
-    updateGovStates [] _ s = s
-    updateGovStates (inj₁ v ∷ vps) k s = updateGovStates vps (suc k) (voteUpdate s v)
-    updateGovStates (inj₂ p ∷ vps) k s = updateGovStates vps (suc k) (propUpdate s p k)
-
-    -- updateGovStates faithfully represents a step of the LEDGER sts
-    STS→GovSt≡ : ∀ {s' : LState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'
-                 → isValid ≡ true → LState.govSt s' ≡ updateGovStates (txgov txb) 0 (LState.govSt s)
-    STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x)))
-      where
-      STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {govSt govSt' : GovState}
-        → (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState ⟧ᵍ , k) govSt vps govSt')
-        → govSt' ≡ updateGovStates vps k govSt
-      STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl
-      STS→updateGovSt≡ (inj₁ v ∷ vps) k {govSt}(BS-ind {s' = .(voteUpdate govSt v)} (GOV-Vote x) h)
-        = STS→updateGovSt≡ vps (suc k) h
-      STS→updateGovSt≡ (inj₂ p ∷ vps) k (BS-ind (GOV-Propose x) h) = STS→updateGovSt≡ vps (suc k) h
-
-  module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
-    open Tx tx renaming (body to txb); open TxBody txb
-    open LEnv Γ renaming (pparams to pp)
-    open PParams pp using (govActionDeposit)
-    govSt : GovState
-    govSt = LState.govSt s
-    open LEDGER-PROPS tx Γ s using (utxoDeps; propUpdate; mkAction; updateGovStates; STS→GovSt≡; voteUpdate)
-    open SetoidReasoning (≡ᵉ-Setoid{DepositPurpose})
-
-    -- No governance action deposits come fro the certs update.
-    noGACerts : (cs : List DCert) (deps : DepositPurpose ⇀ Coin)
-      → filterˢ isGADeposit (dom (updateCertDeposits pp cs deps)) ≡ᵉ filterˢ isGADeposit (dom deps)
-    noGACerts [] _ = filter-pres-≡ᵉ ≡ᵉ.refl
-    noGACerts (c ∷ cs) deps =
-      let  upCD = updateCertDeposits pp cs deps
-           -- open SetoidReasoning (≡ᵉ-Setoid{DepositPurpose})
-      in begin
-      filterˢ isGADeposit (dom (updateCertDeposits pp (c ∷ cs) deps))
-        ≈⟨ filterCR c {upCD ∪⁺ certDeposit c pp} ⟩
-      filterˢ isGADeposit (dom (upCD ∪⁺ certDeposit c pp))
-        ≈⟨ filter-pres-≡ᵉ dom∪⁺≡∪dom ⟩
-      filterˢ isGADeposit (dom upCD ∪ dom (certDeposit c pp))
-        ≈⟨ filter-hom-∪ ⟩
-      filterˢ isGADeposit (dom upCD) ∪ filterˢ isGADeposit (dom (certDeposit c pp))
-        ≈⟨ ∪-cong (noGACerts cs deps) (filterCD pp c) ⟩
-      filterˢ isGADeposit (dom deps) ∪ ∅
-        ≈⟨ ∪-identityʳ (filterˢ isGADeposit (dom deps)) ⟩
-      filterˢ isGADeposit (dom deps) ∎
-
-    dpMap∘voteUpdate≡dpMap : (v : GovVote) {govSt : GovState}
-      → dpMap (voteUpdate govSt v) ≡ dpMap govSt
-    dpMap∘voteUpdate≡dpMap v {[]} = refl
-    dpMap∘voteUpdate≡dpMap v {(aid , ast) ∷ govSt} =
-      cong (λ x → (GovActionDeposit ∘ proj₁) (aid , ast) ∷ x) (dpMap∘voteUpdate≡dpMap v)
-
-    props-dpMap-votes-invar : (vs : List GovVote) (ps : List GovProposal) {k : ℕ} {govSt : GovState}
-      → fromList (dpMap (updateGovStates (map inj₂ ps ++ map inj₁ vs) k govSt ))
-        ≡ᵉ fromList (dpMap (updateGovStates (map inj₂ ps) k govSt))
-    props-dpMap-votes-invar [] ps {k} {govSt} = ≡ᵉ.reflexive
-      (cong (λ x → fromList (dpMap (updateGovStates x k govSt))) (++-identityʳ (map inj₂ ps)))
-    props-dpMap-votes-invar (v ∷ vs) [] {k} {govSt} = begin
-      fromList (dpMap (updateGovStates (map inj₁ (v ∷ vs)) k govSt))
-        ≈⟨ props-dpMap-votes-invar vs [] ⟩
-      fromList (dpMap (updateGovStates (map inj₂ []) (suc k) (voteUpdate govSt v)))
-        ≡⟨ cong fromList (dpMap∘voteUpdate≡dpMap v) ⟩
-      fromList (dpMap govSt)
-        ∎
-    props-dpMap-votes-invar (v ∷ vs) (p ∷ ps) {k} {govSt} = props-dpMap-votes-invar (v ∷ vs) ps
-
-    dpMap-update-∪ : ∀ gSt p k
-      → fromList (dpMap gSt) ∪ ❴ GovActionDeposit (txid , k) ❵
-          ≡ᵉ fromList (dpMap (propUpdate gSt p k))
-    dpMap-update-∪ [] p k = ∪-identityˡ (fromList (dpMap [ mkAction p k ]))
-    dpMap-update-∪ (g@(gaID₀ , gaSt₀) ∷ gSt) p k
-      with (govActionPriority (GovActionState.action gaSt₀))
-           ≤? (govActionPriority (GovActionState.action (proj₂ (mkAction p k))))
-    ... | yes _  = begin
-        fromList (dpMap (g ∷ gSt)) ∪ ❴ GovActionDeposit (txid , k) ❵
-          ≈⟨ ∪-cong fromList-∪-singleton ≡ᵉ.refl ⟩
-        (❴ GovActionDeposit gaID₀ ❵ ∪ fromList (dpMap gSt)) ∪ ❴ GovActionDeposit (txid , k) ❵
-          ≈⟨ ∪-assoc ❴ GovActionDeposit gaID₀ ❵ (fromList (dpMap gSt)) ❴ GovActionDeposit (txid , k) ❵ ⟩
-        ❴ GovActionDeposit gaID₀ ❵ ∪ (fromList (dpMap gSt) ∪ ❴ GovActionDeposit (txid , k) ❵)
-          ≈⟨ ∪-cong ≡ᵉ.refl (dpMap-update-∪ gSt p k) ⟩
-        ❴ GovActionDeposit gaID₀ ❵ ∪ fromList (dpMap (propUpdate gSt p k))
-          ≈˘⟨ fromList-∪-singleton ⟩
-        fromList (dpMap (g ∷ insertGovAction gSt (mkAction p k)))
-          ∎
-    ... | no _   = begin
-        fromList (dpMap (g ∷ gSt)) ∪ ❴ GovActionDeposit (txid , k) ❵
-          ≈⟨ ∪-comm (fromList (dpMap (g ∷ gSt))) ❴ GovActionDeposit (txid , k) ❵ ⟩
-        ❴ GovActionDeposit (txid , k) ❵ ∪ fromList (dpMap (g ∷ gSt))
-          ≈˘⟨ fromList-∪-singleton ⟩
-        fromList (dpMap ((mkAction p k) ∷ g ∷ gSt))
-          ∎
-
-    connex-lemma : ∀ gSt p ps {k}
-      → fromList (dpMap (updateGovStates (map inj₂ ps) k gSt)) ∪ ❴ GovActionDeposit (txid , k + length ps) ❵
-          ≡ᵉ fromList (dpMap (updateGovStates (map inj₂ ps) (suc k) (propUpdate gSt p k)))
-    connex-lemma gSt p [] {k} = begin
-        fromList (dpMap gSt) ∪ ❴ GovActionDeposit (txid , k + 0) ❵
-          ≡⟨ cong (λ x → fromList (dpMap gSt) ∪ ❴ GovActionDeposit (txid , x) ❵) (+-identityʳ k) ⟩
-        fromList (dpMap gSt) ∪ ❴ GovActionDeposit (txid , k) ❵
-          ≈⟨ dpMap-update-∪ gSt p k ⟩
-        fromList (dpMap (propUpdate gSt p k))
-          ∎
-    connex-lemma gSt p (p' ∷ ps) {k} = begin
-      fromList (dpMap (updateGovStates (map inj₂ (p' ∷ ps)) k gSt))
-        ∪ ❴ GovActionDeposit (txid , k + length (p' ∷ ps)) ❵
-          ≡⟨ cong (λ x → fromList (dpMap (updateGovStates (map inj₂ (p' ∷ ps)) k gSt))
-              ∪ ❴ GovActionDeposit (txid , x) ❵) (+-suc k (length ps)) ⟩
-      fromList (dpMap (updateGovStates (map inj₂ ps) (suc k) (propUpdate gSt p' k)))
-        ∪ ❴ GovActionDeposit (txid , (suc k) + length ps) ❵
-          ≈˘⟨ ∪-cong (connex-lemma gSt p' ps) ≡ᵉ.refl ⟩
-      (fromList (dpMap (updateGovStates (map inj₂ ps) k gSt))
-        ∪ ❴ GovActionDeposit (txid , k + length ps) ❵)
-        ∪ ❴ GovActionDeposit (txid , (suc k) + length ps) ❵
-          ≈⟨ ∪-cong (connex-lemma gSt p ps) ≡ᵉ.refl ⟩
-      fromList (dpMap (updateGovStates (map inj₂ ps) (suc k) (propUpdate gSt p k)))
-        ∪ ❴ GovActionDeposit (txid , (suc k) + length ps) ❵
-          ≈⟨ connex-lemma (propUpdate gSt p k) p' ps ⟩
-      fromList (dpMap (updateGovStates (map inj₂ (p' ∷ ps)) (suc k) (propUpdate gSt p k)))
-          ∎
-
-    utxo-govst-connex : ∀ txp {utxoDs gSt gad}
-      → filterˢ isGADeposit (dom (utxoDs)) ≡ᵉ fromList (dpMap gSt)
-      → filterˢ isGADeposit (dom (updateProposalDeposits txp txid gad utxoDs))
-        ≡ᵉ fromList (dpMap (updateGovStates (map inj₂ txp) 0 gSt))
-    utxo-govst-connex [] x = x
-    utxo-govst-connex (p ∷ ps) {utxoDs} {gSt} {gad} x = begin
-      filterˢ isGADeposit (dom (updateProposalDeposits (p ∷ ps) txid gad utxoDs))
-        ≈⟨ filter-pres-≡ᵉ dom∪⁺≡∪dom ⟩
-      filterˢ isGADeposit ((dom (updateProposalDeposits ps txid gad utxoDs))
-        ∪ (dom{X = DepositPurpose ⇀ Coin} ❴ GovActionDeposit (txid , length ps) , gad ❵))
-        ≈⟨ filter-hom-∪ ⟩
-      filterˢ isGADeposit (dom (updateProposalDeposits ps txid gad utxoDs)) ∪ filterˢ isGADeposit
-          (dom{X = DepositPurpose ⇀ Coin} ❴ GovActionDeposit (txid , length ps) , gad ❵)
-        ≈⟨ ∪-cong (utxo-govst-connex ps x) (filter-pres-≡ᵉ dom-single≡single) ⟩
-      fromList (dpMap (updateGovStates (map inj₂ ps) 0 gSt))
-        ∪ filterˢ isGADeposit ❴ GovActionDeposit (txid , length ps) ❵
-        ≈⟨ ∪-cong  ≡ᵉ.refl (filterGA txid _) ⟩
-      fromList (dpMap (updateGovStates (map inj₂ ps) 0 gSt)) ∪ ❴ GovActionDeposit (txid , length ps) ❵
-        ≈⟨ connex-lemma gSt p ps ⟩
-      fromList (dpMap (updateGovStates (map inj₂ (p ∷ ps)) 0 gSt)) ∎
-
-
-  module EPOCH-PROPS (tx : Tx) (Γ : LEnv) (eps : EpochState) where
-    open Tx tx renaming (body to txb); open TxBody txb
-    open LEnv Γ renaming (pparams to pp); open EpochState eps hiding (es); open LState ls
-    open GovActionState; open RatifyState fut using (removed)
-
-    -- GA Deposits Invariance Property for EPOCH STS -----------------------------------------------
-    EPOCH-govDepsMatch :
-      (ratify-removed : mapˢ (GovActionDeposit ∘ proj₁) removed ⊆ mapˢ proj₁ (UTxOState.deposits utxoSt ˢ))
-      (eps' : EpochState) {e : Epoch}
-      → _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
-      → govDepsMatch (EpochState.ls eps) → govDepsMatch (EpochState.ls eps')
-
-    EPOCH-govDepsMatch ratify-removed ⟦ acnt' , ls' ,  es , _ , fut' ⟧ᵉ'
-      (EPOCH x _) = ≡ᵉ.trans (filter-pres-≡ᵉ $ dom-cong (res-comp-cong $ ≡ᵉ.sym χ'≡χ))
-                            ∘ from ≡ᵉ⇔≡ᵉ' ∘ main-invariance-lemma ∘ to ≡ᵉ⇔≡ᵉ'
-      where
-
-      -- the combinator used in the EPOCH rule
-      χ : (DepositPurpose ⇀ Coin) → ℙ DepositPurpose
-      χ deps = mapˢ (proj₁ ∘ proj₂)
-        (flip concatMapˢ removed
-          (λ (gaid , gast) → mapˢ (returnAddr gast ,_) ((deps ∣ ❴ GovActionDeposit gaid ❵) ˢ)))
-
-      -- a simpler combinator that suffices here;
-      χ' : ℙ DepositPurpose
-      χ' = mapˢ (GovActionDeposit ∘ proj₁) removed
-      -- Below we prove χ and χ' are essentially equivalent.
-
-      P : GovActionID × GovActionState → Type
-      P = λ u → proj₁ u ∉ mapˢ proj₁ removed
-
-      P? : Decidable P
-      P? = λ u → ¿ P u ¿
-
-      utxoDeps : Deposits
-      utxoDeps = UTxOState.deposits utxoSt
-
-      -- utxo deposits restricted to new form of set used in EPOCH rule
-      utxoDeps' : Deposits
-      utxoDeps' = utxoDeps ∣ χ' ᶜ
-
-      -- utxo deposits restricted to old form of set used in EPOCH rule
-      utxoDeps'' : Deposits
-      utxoDeps'' = utxoDeps ∣ χ utxoDeps ᶜ
-
-      open Equivalence
-
-      χ'≡χ : χ' ≡ᵉ χ utxoDeps
-      χ'≡χ = χ'⊆χ , χ⊆χ'
-        where
-        χ'⊆χ : χ' ⊆ χ utxoDeps
-        χ'⊆χ {a} x with from ∈-map x
-        ... | (gaid , gast) , refl , gaidgast∈rem with from ∈-map (ratify-removed x)
-        ... | (dp , c) , refl , dpc∈utxoDeps = let gadc = (GovActionDeposit gaid , c) in
-          to ∈-map ((returnAddr gast , gadc)
-                   , refl
-                   , to ∈-concatMapˢ ((gaid , gast)
-                                     , gaidgast∈rem
-                                     , to ∈-map (gadc , refl , res-singleton⁺ {m = utxoDeps} dpc∈utxoDeps)))
-        χ⊆χ' : χ utxoDeps ⊆ χ'
-        χ⊆χ' {a} x with from ∈-map x
-        ... | (rwa , dp , c) , refl , rwa-dp-c∈ with (from ∈-concatMapˢ rwa-dp-c∈)
-        ... | (gaid , gast) , gaid-gast-∈-removed , rwa-dp-c-∈-map with (from ∈-map rwa-dp-c-∈-map)
-        ... | (.dp , _) , refl , q∈ =
-          to ∈-map ((gaid , gast)
-                   , proj₁ (×-≡,≡←≡ (proj₂ (res-singleton'' {m = utxoDeps} q∈)))
-                   , gaid-gast-∈-removed)
-
-
-      map-filter-decomp : ∀ a → (a ∉ χ' × a ∈ˡ map (GovActionDeposit ∘ proj₁) govSt)
-                                 ⇔ (a ∈ˡ map (GovActionDeposit ∘ proj₁)(filter P? govSt))
-      map-filter-decomp a = mk⇔ i (λ h → ii h , iii h)
-        where
-        i : ((a ∉ χ') × (a ∈ˡ map (GovActionDeposit ∘ proj₁) govSt))
-            → a ∈ˡ map (GovActionDeposit ∘ proj₁) (filter P? govSt)
-        i (a∉χ' , a∈) with Inverse.from (map-∈↔ (GovActionDeposit ∘ proj₁)) a∈
-        ... | b , b∈ , refl = Inverse.to (map-∈↔ (GovActionDeposit ∘ proj₁))
-                                         (b , ∈-filter⁺ P? b∈ (a∉χ' ∘ ∈-map⁺-∘) , refl)
-
-        ii : a ∈ˡ map (GovActionDeposit ∘ proj₁) (filter P? govSt) → a ∉ χ'
-        ii a∈ a∈χ' with from (∈ˡ-map-filter{l = govSt}{P? = P?}) a∈
-        ... | _ , _ , refl , Pb with ∈-map⁻' a∈χ'
-        ... | q , refl , q∈rem = Pb (to ∈-map (q , refl , q∈rem))
-
-        iii : a ∈ˡ map (GovActionDeposit ∘ proj₁) (filter P? govSt)
-              → a ∈ˡ map (GovActionDeposit ∘ proj₁) govSt
-        iii a∈ with from (∈ˡ-map-filter{l = govSt}{P? = P?}) a∈
-        ... | b , b∈ , refl , Pb = Inverse.to (map-∈↔ (GovActionDeposit ∘ proj₁)) (b , (b∈ , refl))
-
-
-      main-invariance-lemma :
-          filterˢ isGADeposit (dom utxoDeps) ≡ᵉ' fromList (map (GovActionDeposit ∘ proj₁) govSt)
-          ---------------------------------------------------------------------------------------------------
-        → filterˢ isGADeposit (dom utxoDeps') ≡ᵉ' fromList (map (GovActionDeposit ∘ proj₁) (filter P? govSt))
-
-      main-invariance-lemma HYP a = let open R.EquationalReasoning in
-        a ∈ (filterˢ isGADeposit (dom utxoDeps'))                       ∼⟨ R.SK-sym ∈-filter ⟩
-        (isGADeposit a × a ∈ dom utxoDeps')                             ∼⟨ R.K-refl ×-cong ∈-resᶜ-dom ⟩
-        (isGADeposit a × a ∉ χ' × ∃[ q ] (a , q) ∈ utxoDeps)            ∼⟨ ×-⇔-swap ⟩
-        (a ∉ χ' × isGADeposit a × ∃[ q ] (a , q) ∈ utxoDeps)            ∼⟨ R.K-refl ×-cong (R.K-refl ×-cong dom∈)⟩
-        (a ∉ χ' × isGADeposit a × a ∈ dom utxoDeps)                     ∼⟨ R.K-refl ×-cong ∈-filter ⟩
-        (a ∉ χ' × a ∈ filterˢ isGADeposit (dom utxoDeps))               ∼⟨ R.K-refl ×-cong (HYP a) ⟩
-        (a ∉ χ' × a ∈ fromList (map (GovActionDeposit ∘ proj₁) govSt))  ∼⟨ R.K-refl ×-cong (R.SK-sym ∈-fromList)⟩
-        (a ∉ χ' × a ∈ˡ map (GovActionDeposit ∘ proj₁) govSt)            ∼⟨ map-filter-decomp a ⟩
-        (a ∈ˡ map (GovActionDeposit ∘ proj₁)(filter P? govSt))          ∼⟨ ∈-fromList ⟩
-        a ∈ fromList (map (GovActionDeposit ∘ proj₁)(filter P? govSt))  ∎
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Certs.agda b/src/Ledger/Conway/Foreign/HSLedger/Certs.agda
index c0ba5e932..fa4013f8e 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Certs.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Certs.agda
@@ -2,7 +2,7 @@ module Ledger.Conway.Foreign.HSLedger.Certs where
 
 open import Ledger.Conway.Foreign.HSLedger.Address
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes hiding (DState; CertEnv; GState)
-open import Ledger.Conway.Foreign.HSLedger.Gov
+open import Ledger.Conway.Foreign.HSLedger.Gov.Core
 open import Ledger.Conway.Foreign.HSLedger.PParams
 
 open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; DState; GState)
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Gov.agda b/src/Ledger/Conway/Foreign/HSLedger/Gov.agda
index 882d95a08..5dd303ccd 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Gov.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Gov.agda
@@ -6,28 +6,13 @@ open import Ledger.Conway.Foreign.HSLedger.Address
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes
 open import Ledger.Conway.Foreign.HSLedger.Enact
 open import Ledger.Conway.Foreign.HSLedger.PParams
+open import Ledger.Conway.Foreign.HSLedger.Gov.Core
+open import Ledger.Conway.Foreign.HSLedger.Cert
 
 open import Ledger.Conway.Conformance.Gov it
 open import Ledger.Conway.Conformance.Gov.Properties it
 
-open import Ledger.GovernanceActions govStructure using (Vote) public
-
 instance
-  HsTy-GovRole = autoHsType GovRole
-  Conv-GovRole = autoConvert GovRole
-
-  HsTy-Anchor = autoHsType Anchor
-  Conv-Anchor = autoConvert Anchor
-
-  HsTy-VDeleg = autoHsType VDeleg
-  Conv-VDeleg = autoConvert VDeleg
-
-  HsTy-Vote = autoHsType Vote
-  Conv-Vote = autoConvert Vote
-
-  HsTy-GovVote = autoHsType GovVote
-  Conv-GovVote = autoConvert GovVote
-
   HsTy-GovEnv = autoHsType GovEnv ⊣ withConstructor "MkGovEnv"
                                   • fieldPrefix "ge"
   Conv-GovEnv = autoConvert GovEnv
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Gov/Core.agda b/src/Ledger/Conway/Foreign/HSLedger/Gov/Core.agda
new file mode 100644
index 000000000..2175dcb54
--- /dev/null
+++ b/src/Ledger/Conway/Foreign/HSLedger/Gov/Core.agda
@@ -0,0 +1,22 @@
+module Ledger.Conway.Foreign.HSLedger.Gov.Core where
+
+open import Ledger.Conway.Foreign.HSLedger.Address
+open import Ledger.Conway.Foreign.HSLedger.BaseTypes
+open import Ledger.GovernanceActions govStructure using (Vote) public
+
+instance
+  HsTy-GovRole = autoHsType GovRole
+  Conv-GovRole = autoConvert GovRole
+
+  HsTy-Anchor = autoHsType Anchor
+  Conv-Anchor = autoConvert Anchor
+
+  HsTy-VDeleg = autoHsType VDeleg
+  Conv-VDeleg = autoConvert VDeleg
+
+  HsTy-Vote = autoHsType Vote
+  Conv-Vote = autoConvert Vote
+
+  HsTy-GovVote = autoHsType GovVote
+  Conv-GovVote = autoConvert GovVote
+
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda
index 209ac1311..afd2f7989 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Ratify.agda
@@ -4,6 +4,7 @@ open import Ledger.Conway.Foreign.HSLedger.Address
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes
 open import Ledger.Conway.Foreign.HSLedger.Certs
 open import Ledger.Conway.Foreign.HSLedger.Enact
+open import Ledger.Conway.Foreign.HSLedger.Gov.Core
 open import Ledger.Conway.Foreign.HSLedger.Gov
 
 open import Ledger.Enact govStructure
diff --git a/src/Ledger/Conway/Foreign/HSLedger/Transaction.agda b/src/Ledger/Conway/Foreign/HSLedger/Transaction.agda
index ddad68fa0..9f7942bb4 100644
--- a/src/Ledger/Conway/Foreign/HSLedger/Transaction.agda
+++ b/src/Ledger/Conway/Foreign/HSLedger/Transaction.agda
@@ -3,6 +3,7 @@ module Ledger.Conway.Foreign.HSLedger.Transaction where
 open import Ledger.Conway.Foreign.HSLedger.Address
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes
 open import Ledger.Conway.Foreign.HSLedger.Certs
+open import Ledger.Conway.Foreign.HSLedger.Gov.Core
 open import Ledger.Conway.Foreign.HSLedger.Gov
 open import Ledger.Conway.Foreign.HSLedger.PParams
 
diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda
index 1eed4b954..232f69a43 100644
--- a/src/Ledger/Gov.lagda
+++ b/src/Ledger/Gov.lagda
@@ -6,16 +6,16 @@
 open import Ledger.Types.GovStructure
 open import Ledger.Transaction using (TransactionStructure)
 
-module Ledger.Gov (txs : _) (open TransactionStructure txs using (govStructure)) where
-open GovStructure govStructure hiding (epoch)
+module Ledger.Gov (txs : _) (open TransactionStructure txs hiding (epoch)) where
 
 open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)
 
 open import Axiom.Set.Properties th using (∃-sublist-⇔)
 
-open import Ledger.GovernanceActions govStructure hiding (yes; no)
+open import Ledger.GovernanceActions govStructure using (Vote)
 open import Ledger.Enact govStructure
 open import Ledger.Ratify txs hiding (vote)
+open import Ledger.Certs govStructure
 
 open import Data.List.Ext using (subpermutations; sublists)
 open import Data.List.Ext.Properties2
@@ -43,7 +43,7 @@ GovState = List (GovActionID × GovActionState)
 record GovEnv : Type where
 \end{code}
 \begin{code}[hide]
-  constructor ⟦_,_,_,_,_⟧ᵍ
+  constructor ⟦_,_,_,_,_,_⟧ᵍ
   field
 \end{code}
 \begin{code}
@@ -52,20 +52,9 @@ record GovEnv : Type where
     pparams     : PParams
     ppolicy     : Maybe ScriptHash
     enactState  : EnactState
+    certState   : CertState
 \end{code}
 \end{AgdaMultiCode}
-\emph{Transition relation types}
-\begin{code}[hide]
-data
-\end{code}
-\begin{AgdaSuppressSpace}
-\begin{code}
-  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
-\end{code}
-\begin{code}
-_⊢_⇀⦇_,GOV⦈_     : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
-\end{code}
-\end{AgdaSuppressSpace}
 \begin{code}[hide]
 private variable
   Γ : GovEnv
@@ -80,9 +69,12 @@ private variable
   prev : NeedsHash a
   k : ℕ
   p : Maybe ScriptHash
+
+open GState
+open PState
 \end{code}
 \emph{Functions used in the GOV rules}
-\begin{AgdaMultiCode}
+\begin{AgdaSuppressSpace}
 \begin{code}
 govActionPriority : GovAction → ℕ
 govActionPriority NoConfidence             = 0
@@ -96,14 +88,14 @@ govActionPriority Info                     = 6
 _∼_ : ℕ → ℕ → Type
 n ∼ m = (n ≡ m) ⊎ (n ≡ 0 × m ≡ 1) ⊎ (n ≡ 1 × m ≡ 0)
 
-_≈_ : GovAction → GovAction → Type
-a ≈ a' = (govActionPriority a) ∼ (govActionPriority a')
+_≈ᵍ_ : GovAction → GovAction → Type
+a ≈ᵍ a' = (govActionPriority a) ∼ (govActionPriority a')
 \end{code}
 \begin{code}[hide]
 _∼?_ : (n m : ℕ) → Dec (n ∼ m)
 n ∼? m = n ≟ m ⊎-dec (n ≟ 0 ×-dec m ≟ 1) ⊎-dec (n ≟ 1 ×-dec m ≟ 0)
 
-_≈?_ : (a a' : GovAction) → Dec (a ≈ a')
+_≈?_ : (a a' : GovAction) → Dec (a ≈ᵍ a')
 a ≈? a' = (govActionPriority a) ∼? (govActionPriority a')
 \end{code}
 \begin{code}
@@ -115,11 +107,6 @@ insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
      then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
      else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
 
-addVote : GovState → GovActionID → Voter → Vote → GovState
-addVote s aid voter v = map modifyVotes s
-  where modifyVotes = λ (gid , s') → gid , record s'
-          { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
-
 mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
                  → GovActionID × GovActionState
 mkGovStatePair e aid addr a prev = (aid , record
@@ -129,14 +116,42 @@ addAction : GovState
           → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
           → GovState
 addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)
-
-validHFAction : GovProposal → GovState → EnactState → Type
-validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
-  (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
-  ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
-validHFAction _ _ _ = ⊤
 \end{code}
-\end{AgdaMultiCode}
+\begin{code}[hide]
+opaque
+\end{code}
+\begin{code}
+  addVote : GovState → GovActionID → Voter → Vote → GovState
+  addVote s aid voter v = map modifyVotes s
+    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
+          modifyVotes = λ (gid , s') → gid , record s'
+            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
+
+  isRegistered : GovEnv → Voter → Type
+  isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where
+    CC    → just c ∈ range (gState .ccHotKeys)
+    DRep  → c ∈ dom (gState .dreps)
+    SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
+
+  validHFAction : GovProposal → GovState → EnactState → Type
+  validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
+    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
+    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
+  validHFAction _ _ _ = ⊤
+\end{code}
+\end{AgdaSuppressSpace}
+\emph{Transition relation types}
+\begin{code}[hide]
+data
+\end{code}
+\begin{AgdaSuppressSpace}
+\begin{code}
+  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
+\end{code}
+\begin{code}
+_⊢_⇀⦇_,GOV⦈_     : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
+\end{code}
+\end{AgdaSuppressSpace}
 \caption{Types and functions used in the GOV transition system}
 \label{defs:gov-defs}
 \end{figure*}
@@ -184,7 +199,7 @@ hasParentE e aid a = case getHashES e a of
 hasParent : EnactState → GovState → (a : GovAction) → NeedsHash a → Type
 hasParent e s a aid with getHash aid
 ... | just aid' = hasParentE e aid' a
-                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ a) s
+                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ᵍ a) s
 ... | nothing = ⊤
 \end{code}
 \begin{code}[hide]
@@ -317,6 +332,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
     in
     ∙ (aid , ast) ∈ fromList s
     ∙ canVote pparams (action ast) (proj₁ voter)
+    ∙ isRegistered Γ voter
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
 
diff --git a/src/Ledger/Gov/Properties.agda b/src/Ledger/Gov/Properties.agda
index a79bb5634..af0df6e68 100644
--- a/src/Ledger/Gov/Properties.agda
+++ b/src/Ledger/Gov/Properties.agda
@@ -75,6 +75,9 @@ private
   hasPrev record { action = (TreasuryWdrl _) }        v = no λ ()
   hasPrev record { action = Info }                    v = no λ ()
 
+opaque
+  unfolding validHFAction isRegistered
+
   instance
     validHFAction? : ∀ {p s e} → validHFAction p s e ⁇
     validHFAction? {record { action = NoConfidence }} = Dec-⊤
@@ -93,6 +96,11 @@ private
     validHFAction? {record { action = TreasuryWdrl _ }} = Dec-⊤
     validHFAction? {record { action = Info }} = Dec-⊤
 
+  isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
+  isRegistered? _ (CC   , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (DRep , _) = ¿ _ ∈ _ ¿
+  isRegistered? _ (SPO  , _) = ¿ _ ∈ _ ¿
+
 instance
   Computational-GOV' : Computational _⊢_⇀⦇_,GOV'⦈_ String
   Computational-GOV' = record {Go} where
@@ -103,15 +111,18 @@ instance
       module GoVote sig where
         open GovVote sig
 
-        computeProof = case lookupActionId pparams (proj₁ voter) gid s of λ where
-            (yes p) → case Any↔ .from p of λ where
-              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV))
-            (no ¬p)  → failure (genErrors ¬p)
+        computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
+            (yes p , yes p') → case Any↔ .from p of λ where
+              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
+            (yes _ , no ¬p) → failure (genErrors ¬p)
+            (no ¬p , _)     → failure (genErrors ¬p)
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (GOV-Vote (mem , cV)) with lookupActionId pparams (proj₁ voter) gid s
-        ... | no ¬p = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
-        ... | yes p with Any↔ .from p
+        completeness s' (GOV-Vote (mem , cV , reg))
+          with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
+        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
+        ... | yes _ | no ¬p = ⊥-elim $ ¬p reg
+        ... | yes p | yes p' with Any↔ .from p
         ... | (_ , mem , refl , cV) = refl
 
       module GoProp prop where
diff --git a/src/Ledger/Ledger.lagda b/src/Ledger/Ledger.lagda
index e814a12e4..886a9ddf0 100644
--- a/src/Ledger/Ledger.lagda
+++ b/src/Ledger/Ledger.lagda
@@ -21,6 +21,8 @@ open import Ledger.Utxow txs abs
 open import Ledger.Certs govStructure
 
 open Tx
+open GState
+open GovActionState
 \end{code}
 
 The entire state transformation of the ledger state caused by a valid
@@ -57,6 +59,17 @@ record LState : Type where
 txgov : TxBody → List (GovVote ⊎ GovProposal)
 txgov txb = map inj₂ txprop ++ map inj₁ txvote
   where open TxBody txb
+
+isUnregisteredDRep : CertState → Voter → Type
+isUnregisteredDRep ⟦ _ , _ , gState ⟧ᶜˢ (r , c) = r ≡ DRep × c ∉ dom (gState .dreps)
+
+removeOrphanDRepVotes : CertState → GovActionState → GovActionState
+removeOrphanDRepVotes certState gas = record gas { votes = votes′ }
+  where
+    votes′ = filterKeys (¬_ ∘ isUnregisteredDRep certState) (votes gas)
+
+_|ᵒ_ : GovState → CertState → GovState
+govSt |ᵒ certState = L.map (map₂ (removeOrphanDRepVotes certState)) govSt
 \end{code}
 \end{AgdaMultiCode}
 \caption{Types and functions for the LEDGER transition system}
@@ -98,7 +111,7 @@ data
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     ∙  ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ ⊢ govSt ⇀⦇ txgov txb ,GOV⦈ govSt'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ
 \end{code}
diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda
index 6fdcc59fa..a8d707207 100644
--- a/src/Ledger/Ledger/Properties.agda
+++ b/src/Ledger/Ledger/Properties.agda
@@ -65,14 +65,15 @@ instance
       where
       utxoΓ = UTxOEnv ∋ record { LEnv Γ }
       certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ
-      govΓ  = GovEnv  ∋ ⟦ txid , epoch slot , pparams , ppolicy , enactState ⟧ᵍ
+      govΓ : CertState → GovEnv
+      govΓ = ⟦ txid , epoch slot , pparams , ppolicy , enactState ,_⟧ᵍ
 
       computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')
       computeProof = case isValid ≟ true of λ where
         (yes p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
           (certSt' , certStep) ← computeCerts certΓ certSt txcerts
-          (govSt'  , govStep)  ← computeGov   govΓ  govSt  (txgov txb)
+          (govSt'  , govStep)  ← computeGov (govΓ certSt') (govSt |ᵒ certSt') (txgov txb)
           success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
         (no ¬p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
@@ -87,7 +88,7 @@ instance
       ... | success (utxoSt' , _) | refl
         with computeCerts certΓ certSt txcerts | complete _ _ _ _ certStep
       ... | success (certSt' , _) | refl
-        with computeGov govΓ govSt (txgov txb) | complete govΓ _ _ _ govStep
+        with computeGov (govΓ certSt') (govSt |ᵒ certSt') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certSt') _ _ _ govStep
       ... | success (govSt' , _) | refl = refl
       completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
         with isValid ≟ true
@@ -212,7 +213,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
   mkAction : GovProposal → ℕ → GovActionID × GovActionState
   mkAction p n = let open GovProposal p in
     mkGovStatePair
-      (PParams.govActionLifetime pp +ᵉ (epoch slot))
+      (PParams.govActionLifetime pp +ᵉ epoch slot)
       (txid , n) returnAddr action prevAction
 
   -- update GovState with a proposal
@@ -232,24 +233,54 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
 
   -- updateGovStates faithfully represents a step of the LEDGER sts
   STS→GovSt≡ : ∀ {s' : LState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'
-               → isValid ≡ true → LState.govSt s' ≡ updateGovStates (txgov txb) 0 (LState.govSt s)
+               → isValid ≡ true → LState.govSt s' ≡ updateGovStates (txgov txb) 0 (LState.govSt s |ᵒ LState.certState s')
   STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x)))
     where
-    STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {govSt govSt' : GovState}
-      → (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState ⟧ᵍ , k) govSt vps govSt')
+    STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {certSt : CertState} {govSt govSt' : GovState}
+      → (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt')
       → govSt' ≡ updateGovStates vps k govSt
     STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl
-    STS→updateGovSt≡ (inj₁ v ∷ vps) k {govSt}(BS-ind {s' = .(voteUpdate govSt v)} (GOV-Vote x) h)
+    STS→updateGovSt≡ (inj₁ v ∷ vps) k (BS-ind (GOV-Vote x) h)
       = STS→updateGovSt≡ vps (suc k) h
     STS→updateGovSt≡ (inj₂ p ∷ vps) k (BS-ind (GOV-Propose x) h) = STS→updateGovSt≡ vps (suc k) h
 
+  opaque
+    unfolding addVote
+
+    |ᵒ-[] : ∀ certState → [] |ᵒ certState ≡ []
+    |ᵒ-[] certState = refl
+
+    |ᵒ-++ : ∀ gs gs′ certState → (gs ++ gs′) |ᵒ certState ≡ (gs |ᵒ certState) ++ (gs′ |ᵒ certState)
+    |ᵒ-++ gs gs′ certState = map-++ _ gs gs′
+
+    |ᵒ-singleton : ∀ gid gas certState → ∃[ gas′ ] [ (gid , gas) ] |ᵒ certState ≡ [ (gid , gas′) ]
+    |ᵒ-singleton gid gas certState = (removeOrphanDRepVotes certState gas , refl)
+
+    dpMap-|ᵒ-singleton : ∀ g certState → dpMap ([ g ] |ᵒ certState) ≡ dpMap [ g ]
+    dpMap-|ᵒ-singleton (gid , gas) certState rewrite |ᵒ-singleton gid gas certState .proj₂ = refl
+
+    dpMap-|ᵒ : ∀ govSt certState → dpMap (govSt |ᵒ certState) ≡ dpMap govSt
+    dpMap-|ᵒ [] certState = cong dpMap (|ᵒ-[] certState)
+    dpMap-|ᵒ (g ∷ govSt) certState = let open ≡-Reasoning in begin
+      dpMap ((g ∷ govSt) |ᵒ certState)
+        ≡⟨ cong dpMap (|ᵒ-++ [ g ] govSt certState) ⟩
+      dpMap (([ g ] |ᵒ certState) ++ (govSt |ᵒ certState))
+        ≡⟨ map-++ _ ([ g ] |ᵒ certState) (govSt |ᵒ certState) ⟩
+      dpMap ([ g ] |ᵒ certState) ++ dpMap (govSt |ᵒ certState)
+        ≡⟨ cong (dpMap ([ g ] |ᵒ certState) ++_) (dpMap-|ᵒ govSt certState) ⟩
+      dpMap ([ g ] |ᵒ certState) ++ dpMap govSt
+        ≡⟨ cong (_++ dpMap govSt) (dpMap-|ᵒ-singleton g certState) ⟩
+      dpMap [ g ] ++ dpMap govSt
+        ≡˘⟨ map-++ _ [ g ] govSt ⟩
+      dpMap (g ∷ govSt) ∎
+
 module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
   open Tx tx renaming (body to txb); open TxBody txb
   open LEnv Γ renaming (pparams to pp)
   open PParams pp using (govActionDeposit; poolDeposit)
   govSt : GovState
   govSt = LState.govSt s
-  open LEDGER-PROPS tx Γ s using (utxoDeps; propUpdate; mkAction; updateGovStates; STS→GovSt≡; voteUpdate)
+  open LEDGER-PROPS tx Γ s using (utxoDeps; propUpdate; mkAction; updateGovStates; STS→GovSt≡; voteUpdate; dpMap-|ᵒ)
   open SetoidReasoning (≡ᵉ-Setoid{DepositPurpose})
 
   CredDepIsNotGADep : ∀ {a c} → a ≡ CredentialDeposit c → ¬ isGADeposit a
@@ -342,11 +373,14 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
   noGACerts (retirepool _ _ ∷ cs) deps = noGACerts cs deps
   noGACerts (ccreghot _ _ ∷ cs) deps = noGACerts cs deps
 
-  dpMap∘voteUpdate≡dpMap : (v : GovVote) {govSt : GovState}
-    → dpMap (voteUpdate govSt v) ≡ dpMap govSt
-  dpMap∘voteUpdate≡dpMap v {[]} = refl
-  dpMap∘voteUpdate≡dpMap v {(aid , ast) ∷ govSt} =
-    cong (λ x → (GovActionDeposit ∘ proj₁) (aid , ast) ∷ x) (dpMap∘voteUpdate≡dpMap v)
+  opaque
+    unfolding addVote
+
+    dpMap∘voteUpdate≡dpMap : (v : GovVote) {govSt : GovState}
+      → dpMap (voteUpdate govSt v) ≡ dpMap govSt
+    dpMap∘voteUpdate≡dpMap v {[]} = refl
+    dpMap∘voteUpdate≡dpMap v {(aid , ast) ∷ govSt} =
+      cong (λ x → (GovActionDeposit ∘ proj₁) (aid , ast) ∷ x) (dpMap∘voteUpdate≡dpMap v)
 
   props-dpMap-votes-invar : (vs : List GovVote) (ps : List GovProposal) {k : ℕ} {govSt : GovState}
     → fromList (dpMap (updateGovStates (map inj₂ ps ++ map inj₁ vs) k govSt ))
@@ -437,6 +471,60 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
       ≈⟨ connex-lemma gSt p ps ⟩
     fromList (dpMap (updateGovStates (map inj₂ (p ∷ ps)) 0 gSt)) ∎
 
+  -- The list of natural numbers from 0 up to `n` - 1.
+  ⟦0:<_⟧ : ℕ → List ℕ
+  ⟦0:< 0     ⟧ = []
+  ⟦0:< suc n ⟧ = ⟦0:< n ⟧ ++ [ n ]
+
+  connex-lemma-rep : ∀ k govSt ps →
+    fromList (dpMap (updateGovStates (map inj₂ ps) k govSt))
+    ≡ᵉ
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧)
+  connex-lemma-rep k govSt [] = begin
+    fromList (dpMap govSt)
+      ≈˘⟨ ∪-identityʳ (fromList (dpMap govSt)) ⟩
+    fromList (dpMap govSt) ∪ fromList []
+      ≡⟨⟩
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< 0 ⟧) ∎
+  connex-lemma-rep k govSt (p ∷ ps) = begin
+    fromList (dpMap (updateGovStates (map inj₂ (p ∷ ps)) k govSt))
+      ≡⟨⟩
+    fromList (dpMap (updateGovStates (inj₂ p ∷ map inj₂ ps) k govSt))
+      ≡⟨⟩
+    fromList (dpMap (updateGovStates (map inj₂ ps) (suc k) (propUpdate govSt p k)))
+      ≈˘⟨ connex-lemma govSt p ps {k} ⟩
+    fromList (dpMap (updateGovStates (map inj₂ ps) k govSt)) ∪ ❴ GovActionDeposit (txid , k + length ps) ❵
+      ≈⟨ ∪-cong (connex-lemma-rep k govSt ps) ≡ᵉ.refl ⟩
+    (fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧)) ∪ ❴ GovActionDeposit (txid , k + length ps) ❵
+      ≈⟨ ∪-assoc (fromList (dpMap govSt)) (fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧)) ❴ GovActionDeposit (txid , k + length ps) ❵ ⟩
+    fromList (dpMap govSt) ∪ (fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧) ∪ ❴ GovActionDeposit (txid , k + length ps) ❵)
+      ≡⟨⟩
+    fromList (dpMap govSt) ∪ (fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧) ∪ fromList [ GovActionDeposit (txid , k + length ps) ])
+      ≈⟨ ∪-cong ≡ᵉ.refl (∪-fromList-++ (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧) [ GovActionDeposit (txid , k + length ps) ]) ⟩
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length ps ⟧ ++ [ GovActionDeposit (txid , k + length ps) ])
+      ≡˘⟨ cong (λ x → fromList (dpMap govSt) ∪ fromList x) (map-++ _ ⟦0:< length ps ⟧ [ length ps ]) ⟩
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) (⟦0:< length ps ⟧ ++ [ length ps ]))
+      ≡⟨⟩
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length (p ∷ ps) ⟧) ∎
+
+  -- Removing orphan DRep votes does not modify the set of GAs in GovState
+  |ᵒ-GAs-pres : ∀ k govSt certState →
+    fromList (dpMap (updateGovStates (txgov txb) k (govSt |ᵒ certState)))
+    ≡ᵉ
+    fromList (dpMap (updateGovStates (txgov txb) k govSt))
+  |ᵒ-GAs-pres k govSt certState = begin
+    fromList (dpMap (updateGovStates (txgov txb) k (govSt |ᵒ certState)))
+      ≈⟨ props-dpMap-votes-invar txvote txprop {k} {govSt |ᵒ certState} ⟩
+    fromList (dpMap (updateGovStates (map inj₂ txprop) k (govSt |ᵒ certState)))
+      ≈⟨ connex-lemma-rep k (govSt |ᵒ certState) txprop ⟩
+    fromList (dpMap (govSt |ᵒ certState)) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length txprop ⟧)
+      ≡⟨ cong (λ x → fromList x ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length txprop ⟧)) (dpMap-|ᵒ govSt certState) ⟩
+    fromList (dpMap govSt) ∪ fromList (map (λ i → GovActionDeposit (txid , k + i)) ⟦0:< length txprop ⟧)
+      ≈˘⟨ connex-lemma-rep k govSt txprop ⟩
+    fromList (dpMap (updateGovStates (map inj₂ txprop) k govSt))
+      ≈˘⟨ props-dpMap-votes-invar txvote txprop {k} {govSt} ⟩
+    fromList (dpMap (updateGovStates (txgov txb) k govSt)) ∎
+
   -- GA Deposits Invariance Property for LEDGER STS ----------------------------------------------------
   LEDGER-govDepsMatch : ∀ {s' : LState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'
                         → govDepsMatch s → govDepsMatch s'
@@ -444,7 +532,7 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
 
   LEDGER-govDepsMatch s'@{⟦ .(⟦ ((UTxOState.utxo (LState.utxoSt s) ∣ txins ᶜ) ∪ˡ (outs txb))
                               , _ , updateDeposits pp txb (UTxOState.deposits (LState.utxoSt s)) , _ ⟧ᵘ)
-                          , govSt' , _ ⟧ˡ}
+                          , govSt' , certState' ⟧ˡ}
     utxosts@(LEDGER-V⋯ tx-valid (UTXOW-UTXOS (Scripts-Yes x)) _ GOV-sts) aprioriMatch = begin
       filterˢ isGADeposit (dom (updateDeposits pp txb utxoDeps))
         ≈⟨ noGACerts txcerts (updateProposalDeposits txprop txid govActionDeposit utxoDeps) ⟩
@@ -453,6 +541,8 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
       fromList (dpMap (updateGovStates (map inj₂ txprop) 0 govSt))
         ≈˘⟨ props-dpMap-votes-invar txvote txprop ⟩
       fromList (dpMap (updateGovStates (txgov txb) 0 govSt ))
+        ≈˘⟨ |ᵒ-GAs-pres 0 govSt certState' ⟩
+      fromList (dpMap (updateGovStates (txgov txb) 0 (govSt |ᵒ certState')))
         ≡˘⟨ cong (fromList ∘ dpMap ) (STS→GovSt≡ utxosts tx-valid) ⟩
       fromList (dpMap govSt') ∎
 
diff --git a/src/Ledger/hs-src/Lib.hs b/src/Ledger/hs-src/Lib.hs
index 6367b50ae..69de8f0cf 100644
--- a/src/Ledger/hs-src/Lib.hs
+++ b/src/Ledger/hs-src/Lib.hs
@@ -24,9 +24,10 @@ import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Enact       as X
   (EnactState(..), EnactEnv(..), enactStep, GovAction (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Epoch       as X
   (Snapshot(..), Snapshots(..), EpochState(..), epochStep)
+import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Gov.Core    as X
+  (GovRole(..), Anchor(..), VDeleg(..), Vote(..), GovVote(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Gov         as X
-  ( GovRole(..), Anchor(..), VDeleg(..), Vote(..), GovVote(..), GovEnv(..), GovProposal(..)
-  , GovActionState(..), govStep, GovState, GovActionID, Voter)
+  ( GovEnv(..), GovProposal(..), GovActionState(..), govStep, GovState, GovActionID, Voter)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.Ledger      as X
   (LEnv(..), LState(..), ledgerStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.HSLedger.NewEpoch    as X