diff --git a/CHANGELOG.md b/CHANGELOG.md
index d4f0895f40..b6b7a281ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,7 @@
 
 ## Conway spec
 
+- Remove POST-CERT; delegated stake for voting is now removed by GOVCERT at the moment of deregistration
 - Move `txIns ∩ refInputs ≡ ∅` precondition to `allowedLanguages` to allow non-disjoint tx and ref. inputs for Plutus V1-V2
 - Require collateral inputs to be present in the UTxO set in the UTXO rule
 - State and prove the claim that a voter's (last) vote in a block is applied to the governance action (see #417)
diff --git a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Conway/Foreign/API.hs b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Conway/Foreign/API.hs
index 512af8e8b6..540e16f340 100644
--- a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Conway/Foreign/API.hs
+++ b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Conway/Foreign/API.hs
@@ -12,11 +12,11 @@ import MAlonzo.Code.Ledger.Conway.Foreign.Transaction       as X
   , Script, Datum, DataHash, Value, TxOut, RdmrPtr, ScriptHash, AuxiliaryData, Withdrawals
   , HSTimelock (..), HSPlutusScript (..))
 import MAlonzo.Code.Ledger.Conway.Foreign.Cert              as X
-  (certStep, certsStep, CertState(..))
+  (certStep, certsStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.Chain             as X
   (ChainState(..), HSBlock(..), chainStep)
 import MAlonzo.Code.Ledger.Conway.Foreign.Certs             as X
-  ( StakePoolParams(..), PState(..), DelegEnv(..), CertEnv(..), DState(..), DCert(..), GState(..)
+  ( StakePoolParams(..), PState(..), DelegEnv(..), CertEnv(..), DState(..), DCert(..), GState(..), CertState(..)
   , delegStep, govCertStep, poolStep, DepositPurpose(..))
 import MAlonzo.Code.Ledger.Conway.Foreign.Enact             as X
   (EnactState(..), EnactEnv(..), enactStep)
diff --git a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs
index f43567fce9..7e3fdc7e61 100644
--- a/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs
+++ b/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs
@@ -17,11 +17,11 @@ import MAlonzo.Code.Ledger.Dijkstra.Foreign.Transaction       as X
   , Redeemer, RedeemerPtr
   , NativeScript(..), HSNativeScript (..), HSPlutusScript (..))
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Cert              as X
-  (certStep, certsStep, CertState(..))
+  (certStep, certsStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Chain             as X
   (ChainState(..), Block(..), chainStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Certs             as X
-  ( StakePoolParams(..), PState(..), DelegEnv(..), GovCertEnv(..), CertEnv(..), DState(..), DCert(..), GState(..)
+  ( StakePoolParams(..), PState(..), DelegEnv(..), GovCertEnv(..), CertEnv(..), DState(..), DCert(..), GState(..), CertState(..)
   , delegStep, govCertStep, poolStep)
 import MAlonzo.Code.Ledger.Dijkstra.Foreign.Entities          as X
   (EntitiesEnv(..), entitiesStep, SubEntitiesEnv(..), subentitiesStep)
diff --git a/src/Interface/ComputationalRelation.lagda.md b/src/Interface/ComputationalRelation.lagda.md
index 40a85f2162..92c49ab0cf 100644
--- a/src/Interface/ComputationalRelation.lagda.md
+++ b/src/Interface/ComputationalRelation.lagda.md
@@ -583,3 +583,27 @@ module _ {Init : C → S → ⊤ → S → Type} ⦃ _ : Computational Init Err
               | completeness {Err = Err} _ _ _ _ rtat
         ...   | success (t' , r) | refl = refl
 ```
+
+```agda
+module _ {Init : C → S → ⊤ → S → Type} ⦃ _ : Computational Init Err₂ ⦄ where
+  module _ {Step : C → S → Sig → S → Type} ⦃ _ : Computational Step Err₁ ⦄
+           ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where
+
+    instance
+      Computational-RunTraceAfter : Computational (RunTraceAfter Init Step) Err
+
+      Computational-RunTraceAfter .computeProof Γ s sigs
+        with computeProof {STS = Init} Γ s tt
+      ... | failure e = failure (injectError it e)
+      ... | success (s' , h)
+            with computeProof {STS = ReflexiveTransitiveClosure {sts = Step}} {Err = Err} Γ s' sigs
+      ...   | failure e = failure e
+      ...   | success (t , r) = success (t , run (h , r))
+
+      Computational-RunTraceAfter .completeness Γ s sigs t (run (init , rtc))
+        with computeProof {STS = Init} Γ s tt | completeness _ _ _ _ init
+      ... | success (s' , h) | refl
+            with computeProof {STS = ReflexiveTransitiveClosure {sts = Step}} {Err = Err} Γ s' sigs
+            | completeness {Err = Err} _ _ _ _ rtc
+      ...   | success (t' , r) | refl = refl
+```
diff --git a/src/Interface/STS.lagda.md b/src/Interface/STS.lagda.md
index f19096721e..128a1d42cb 100644
--- a/src/Interface/STS.lagda.md
+++ b/src/Interface/STS.lagda.md
@@ -40,6 +40,9 @@ does—it processes a list of signals, transforming state.
    +  `RunTraceAfterAndThen`: run a given transition (`Init`), then run a transition
       (`Step`) for a each signal in a given list, then, once the list is empty, run a
       final (`Last`) transition.
+   +  `RunTraceAfter`: run a given transition (`Init`), then run a transition (`Step`)
+      for each signal in a given list. This is `RunTraceAfterAndThen` with a trivial
+      final transition, built on the reflexive-transitive closure of `Step`.
 
 ## High-level picture
 
@@ -142,6 +145,20 @@ ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_
 ReflexiveTransitiveClosureᵇ = _⊢_⇀⟦_⟧*_
 ```
 
+### Running a Trace After an Initial Transition
+
+```agda
+data RunTraceAfter (Init : C → S → ⊤ → S → Type)
+                   (Step : C → S → Sig → S → Type) :
+  C → S → List Sig → S → Type where
+
+    run :
+        ∙ Init Γ s tt s'
+        ∙ ReflexiveTransitiveClosure {sts = Step} Γ s' sigs s''
+        ─────────────────────────────────────────────
+        RunTraceAfter Init Step Γ s sigs s''
+```
+
 ## Totality
 
 We say a single-step relation is **total** if every input has some output.
diff --git a/src/Ledger/Conway/Conformance/Certs.lagda.md b/src/Ledger/Conway/Conformance/Certs.lagda.md
index 7d8e9a64f2..1602a5549a 100644
--- a/src/Ledger/Conway/Conformance/Certs.lagda.md
+++ b/src/Ledger/Conway/Conformance/Certs.lagda.md
@@ -19,7 +19,7 @@ private module Certs = Ledger.Conway.Specification.Certs gs
 open Certs public
   hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
           _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
-          _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,POST-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
+          _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
 open RewardAddress
 
 record DState : Type where
@@ -105,6 +105,7 @@ private variable
   stᵈ stᵈ' : DState
   stᵍ stᵍ' : GState
   stᵖ stᵖ' : PState
+  stᶜ stᶜ' : CertState
 
 open GovVote
 
@@ -149,31 +150,31 @@ data _⊢_⇀⦇_,DELEG⦈_ where
         ⟦ vDelegs , sDelegs , rwds ∪ˡ ❴ c , 0 ❵
         , updateCertDeposit pp (reg c d) dep ⟧
 
-data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where
+data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
   GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
     ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢
-      ⟦ dReps , ccKeys , dep ⟧
+      ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
         ⇀⦇ regdrep c d an ,GOVCERT⦈
-      ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
-      , updateCertDeposit pp (regdrep c d an ) dep ⟧
+      ⟦ stᵈ , stᵖ , ⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
+      , updateCertDeposit pp (regdrep c d an ) dep ⟧ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
     ∙ (DRepDeposit c , d) ∈ dep
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , dep ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ vDelegs , sDelegs , rwds , ddep ⟧ᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
           ⇀⦇ deregdrep c d ,GOVCERT⦈
-          ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧
+          ⟦ ⟦ vDelegs ∣^ ❴ vDelegCredential c ❵ ᶜ , sDelegs , rwds , ddep ⟧ᵈ , stᵖ , ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , updateCertDeposit pp (deregdrep c d) dep ⟧ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys , dep ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , dep ⟧ ⟧
           ⇀⦇ ccreghot c mc ,GOVCERT⦈
-          ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧
+          ⟦ stᵈ , stᵖ , ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , updateCertDeposit pp (ccreghot c mc) dep ⟧ ⟧
 
 data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
   CERT-deleg :
@@ -187,9 +188,9 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → T
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-vdel :
-    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
+    ∙ Γ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
       ────────────────────────────────
-      Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
+      Γ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'
 
 data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
 
@@ -206,15 +207,6 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
       ⇀⦇ _ ,PRE-CERT⦈
       ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards , ddep ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys , gdep ⟧ ⟧
 
-data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
-
-  CERT-post :
-      ⟦ e , pp , vs , wdrls , cc ⟧
-      ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧ , stᵖ , stᵍ ⟧
-        ⇀⦇ _ ,POST-CERT⦈
-        ⟦ ⟦ voteDelegs ∣^ (mapˢ vDelegCredential (dom (GState.dreps stᵍ)) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []))
-          , stakeDelegs , rewards , ddep ⟧ , stᵖ , stᵍ ⟧
-
 _⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
-_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_
+_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfter _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_
 ```
diff --git a/src/Ledger/Conway/Conformance/Certs/Properties.lagda.md b/src/Ledger/Conway/Conformance/Certs/Properties.lagda.md
index 1968b52f17..0c130b3fb4 100644
--- a/src/Ledger/Conway/Conformance/Certs/Properties.lagda.md
+++ b/src/Ledger/Conway/Conformance/Certs/Properties.lagda.md
@@ -84,41 +84,41 @@ instance
     rewrite dec-yes (¿ c ∉ dom (DState.rewards ds) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
-  Computational-GOVCERT .computeProof ce gs (regdrep c d _) =
-    let open CertEnv ce; open GState gs; open PParams pp in
-    case ¿ (d ≡ drepDeposit × c ∉ dom dreps)
-         ⊎ (d ≡ 0 × c ∈ dom dreps) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (regdrep c d _) =
+    let open CertEnv ce; open PParams pp in
+    case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps (CertState.gState cs)))
+         ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (CertState.gState cs))) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (deregdrep c d) =
-    case ¿ c ∈ dom (GState.dreps gs) × (DRepDeposit c , d) ∈  (GState.deposits gs) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (deregdrep c d) =
+    case ¿ c ∈ dom (GState.dreps (CertState.gState cs)) × (DRepDeposit c , d) ∈  (GState.deposits (CertState.gState cs)) ¿ of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (ccreghot c _) =
-    let open CertEnv ce; open GState gs in
-    case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (ccreghot c _) =
+    let open CertEnv ce in
+    case ¿ ((c , nothing) ∉ GState.ccHotKeys (CertState.gState cs) ˢ) × c ∈ coldCreds ¿ of λ where
       (yes p) → success (-, GOVCERT-ccreghot p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
-  Computational-GOVCERT .completeness ce gs
+  Computational-GOVCERT .completeness ce cs
     (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
       ¿ (let open CertEnv ce; open PParams pp in
-        (d ≡ drepDeposit × c ∉ dom (GState.dreps gs)) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps gs)))
+        (d ≡ drepDeposit × c ∉ dom (GState.dreps (CertState.gState cs))) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (CertState.gState cs))))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness _ gs
+  Computational-GOVCERT .completeness _ cs
     (deregdrep c d) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes ¿ c ∈ dom (GState.dreps gs) × (DRepDeposit c , d) ∈ (GState.deposits gs) ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness ce gs
+    rewrite dec-yes ¿ c ∈ dom (GState.dreps (CertState.gState cs)) × (DRepDeposit c , d) ∈ (GState.deposits (CertState.gState cs)) ¿ p .proj₂ = refl
+  Computational-GOVCERT .completeness ce cs
     (ccreghot c _) _ (GOVCERT-ccreghot p)
-    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys gs) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
+    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys (CertState.gState cs)) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
 
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
   Computational-CERT .computeProof ce cs dCert
     with computeProof ⟦ CertEnv.pp ce , PState.pools (CertState.pState cs) , dom (GState.dreps (CertState.gState cs)) ⟧
                       (CertState.dState cs) dCert
          | computeProof (CertEnv.pp ce) (CertState.pState cs) dCert
-         | computeProof ce (CertState.gState cs) dCert
+         | computeProof ce cs dCert
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
   ... | failure _       | failure _       | success (_ , h) = success (-, CERT-vdel h)
@@ -153,15 +153,15 @@ instance
   Computational-CERT .completeness Γ cs
     dCert@(regdrep c d an)
     cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
+    with computeProof {STS = _⊢_⇀⦇_,GOVCERT⦈_} Γ cs dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
   Computational-CERT .completeness Γ cs
     dCert@(deregdrep c _) cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
+    with computeProof {STS = _⊢_⇀⦇_,GOVCERT⦈_} Γ cs dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
   Computational-CERT .completeness Γ cs
     dCert@(ccreghot c mkh) cs' (CERT-vdel h)
-    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
+    with computeProof {STS = _⊢_⇀⦇_,GOVCERT⦈_} Γ cs dCert | completeness _ _ _ _ h
   ... | success _ | refl = refl
 
 
@@ -181,23 +181,6 @@ instance
                 × mapˢ (map₁ RewardAddress.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
-  -- POST-CERT has no premises, so computing always succeeds
-  -- with the unique post-state and proof CERT-post.
-  Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
-  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
-    where
-      dreps : DReps
-      dreps = GState.dreps (CertState.gState cs)
-      validVoteDelegs : VoteDelegs
-      validVoteDelegs = (DState.voteDelegs (CertState.dState cs)) ∣^ ( mapˢ vDelegCredential (dom dreps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
-      cs' : CertState
-      cs' = ⟦ ⟦ validVoteDelegs , _ , _ ⟧ , CertState.pState cs , CertState.gState cs ⟧
-
-  -- Completeness: the relational proof pins s' to exactly `post`,
-  -- and computeProof returns success at that same state; so refl.
-  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
-
-
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it
 ```
diff --git a/src/Ledger/Conway/Conformance/Equivalence.lagda.md b/src/Ledger/Conway/Conformance/Equivalence.lagda.md
index cbbbd14732..43939f61a3 100644
--- a/src/Ledger/Conway/Conformance/Equivalence.lagda.md
+++ b/src/Ledger/Conway/Conformance/Equivalence.lagda.md
@@ -188,26 +188,26 @@ WellformedLState s = certDepositsC (C.LState.certState s) ≡ᵈ certDeposits (c
 
 getValidCertDepositsCERTS : ∀ {Γ s certs s'} deposits (open L.CertEnv Γ using (pp))
                           → certDepositsC s ≡ᵈ (certDDeps deposits , certGDeps deposits)
-                          → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s certs s'
+                          → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s certs s'
                           → L.ValidCertDeposits pp deposits certs
-getValidCertDepositsCERTS deposits wf (run-[] x) = L.[]
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-deleg (C.DELEG-delegate x)) rs)
+getValidCertDepositsCERTS deposits wf (BS-base x) = L.[]
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-delegate x)) rs)
   = L.delegate (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-deleg (C.DELEG-dereg (_ , h , h'))) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-dereg (_ , h , h'))) rs)
   = L.dereg (∈-filter .Equivalence.from (wf .proj₁ .proj₁ h) .proj₂) h'
             (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-deleg (C.DELEG-reg x)) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-reg x)) rs)
   = L.reg (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-pool L.POOL-regpool) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-pool L.POOL-regpool) rs)
   = L.regpool (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-pool C.POOL-retirepool) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-pool C.POOL-retirepool) rs)
   = L.retirepool (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-vdel (C.GOVCERT-regdrep x)) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-vdel (C.GOVCERT-regdrep x)) rs)
   = L.regdrep (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-vdel (C.GOVCERT-deregdrep (_ , h))) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-vdel (C.GOVCERT-deregdrep (_ , h))) rs)
   = L.deregdrep (∈-filter .Equivalence.from (wf .proj₂ .proj₁ h) .proj₂)
                 (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
-getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (run-∷ (C.CERT-vdel (C.GOVCERT-ccreghot x)) rs)
+getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot x)) rs)
   = L.ccreghot(getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 
 
@@ -269,17 +269,17 @@ instance
 open IsEquivalence ≡ᵈ-isEquivalence renaming (refl to ≡ᵈ-refl; sym to ≡ᵈ-sym; trans to ≡ᵈ-trans)
 
 lemCERTS'DepositsC : ∀ {Γ s dcerts s'} (open C.CertEnv Γ using (pp))
-                   → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
+                   → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s'
                    → certDepositsC s' ≡ ⟨ updateDDeps pp dcerts , updateGDeps pp dcerts ⟩ (certDepositsC s)
-lemCERTS'DepositsC (run-[] C.CERT-post) = refl
-lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-delegate     _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-dereg        _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-deleg  (C.DELEG-reg          _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-pool   L.POOL-regpool          ) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-pool    C.POOL-retirepool     )  rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-regdrep    _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-deregdrep  _)) rs) = lemCERTS'DepositsC rs
-lemCERTS'DepositsC (run-∷ (C.CERT-vdel   (C.GOVCERT-ccreghot   _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-base Id-nop) = refl
+lemCERTS'DepositsC (BS-ind (C.CERT-deleg  (C.DELEG-delegate     _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-deleg  (C.DELEG-dereg        _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-deleg  (C.DELEG-reg          _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-pool   L.POOL-regpool          ) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-pool    C.POOL-retirepool     )  rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-vdel   (C.GOVCERT-regdrep    _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-vdel   (C.GOVCERT-deregdrep  _)) rs) = lemCERTS'DepositsC rs
+lemCERTS'DepositsC (BS-ind (C.CERT-vdel   (C.GOVCERT-ccreghot   _)) rs) = lemCERTS'DepositsC rs
 
 lemCERTSDepositsC : ∀ {Γ s txCerts s'} (open C.CertEnv Γ using (pp))
                   → Γ C.⊢ s ⇀⦇ txCerts ,CERTS⦈ s'
@@ -338,54 +338,54 @@ updateCDep pp cert (ddep , gdep) = updateDDep pp cert ddep , updateGDep pp cert
 opaque
   castCERTS' : ∀ {Γ certs} {s s' : L.CertState} deps₁ deps₂ deps₁'
              → deps₁ ≡ᵈ deps₂
-             → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ (deps₁ ⊢conv s) certs (deps₁' ⊢conv s')
+             → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ (deps₁ ⊢conv s) certs (deps₁' ⊢conv s')
              → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂'
-                           × RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ (deps₂ ⊢conv s) certs (deps₂' ⊢conv s')
-  castCERTS' deps₁ deps₂ deps₁' eqd (run-[] C.CERT-post) = deps₂ , eqd , run-[] C.CERT-post
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-deleg {dCert = cert} (C.DELEG-delegate h))    rs)
+                           × ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ (deps₂ ⊢conv s) certs (deps₂' ⊢conv s')
+  castCERTS' deps₁ deps₂ deps₁' eqd (BS-base Id-nop) = deps₂ , eqd , BS-base Id-nop
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-delegate h))    rs)
     = let
         open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-        in  deps₂' , eqd' , run-∷ (C.CERT-deleg (C.DELEG-delegate h)) rs'
+        in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-delegate h)) rs'
 
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-deleg {dCert = cert} (C.DELEG-dereg (a , b , c))) rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-dereg (a , b , c))) rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-deleg (C.DELEG-dereg (a , eqd .proj₁ .proj₁ b , c))) rs'
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-deleg {dCert = cert} (C.DELEG-reg h))         rs) =
+    in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-dereg (a , eqd .proj₁ .proj₁ b , c))) rs'
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-reg h))         rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-deleg (C.DELEG-reg h)) rs'
+    in  deps₂' , eqd' , BS-ind (C.CERT-deleg (C.DELEG-reg h)) rs'
 
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-pool  {dCert = cert} L.POOL-regpool)          rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-pool  {dCert = cert} L.POOL-regpool)          rs) =
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs
-    in  deps₂' , eqd' , run-∷  (C.CERT-pool L.POOL-regpool) rs'
+    in  deps₂' , eqd' , BS-ind  (C.CERT-pool L.POOL-regpool) rs'
 
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-pool  {dCert = cert} C.POOL-retirepool)       rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-pool  {dCert = cert} C.POOL-retirepool)       rs) =
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-pool C.POOL-retirepool) rs'
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-vdel  {dCert = cert} (C.GOVCERT-regdrep h))   rs) =
+    in  deps₂' , eqd' , BS-ind (C.CERT-pool C.POOL-retirepool) rs'
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-vdel  {dCert = cert} (C.GOVCERT-regdrep h))   rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-vdel (C.GOVCERT-regdrep h)) rs'
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-vdel  {dCert = cert} (C.GOVCERT-deregdrep (a , b))) rs) =
+    in  deps₂' , eqd' , BS-ind (C.CERT-vdel (C.GOVCERT-regdrep h)) rs'
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-vdel  {dCert = cert} (C.GOVCERT-deregdrep (a , b))) rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
                                          (⟨ cong-updateDDep {pp} cert {deps₁ .proj₁} {deps₂ .proj₁}
                                           , cong-updateGDep {pp} cert {deps₁ .proj₂} {deps₂ .proj₂} ⟩ eqd) rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-vdel (C.GOVCERT-deregdrep (a , eqd .proj₂ .proj₁ b))) rs'
+    in  deps₂' , eqd' , BS-ind (C.CERT-vdel (C.GOVCERT-deregdrep (a , eqd .proj₂ .proj₁ b))) rs'
                                                                    -- ^^^^^^^^^^^^^^^^^^^ Actual work
-  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (run-∷ (C.CERT-vdel  {dCert = cert} (C.GOVCERT-ccreghot h))  rs) =
+  castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-vdel  {dCert = cert} (C.GOVCERT-ccreghot h))  rs) =
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs
-    in  deps₂' , eqd' , run-∷ (C.CERT-vdel (C.GOVCERT-ccreghot h)) rs'
+    in  deps₂' , eqd' , BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot h)) rs'
 
   castCERTS : ∀ {Γ certs} {s s' : L.CertState} deps₁ deps₂ deps₁'
             → deps₁ ≡ᵈ deps₂
diff --git a/src/Ledger/Conway/Conformance/Equivalence/Certs.lagda.md b/src/Ledger/Conway/Conformance/Equivalence/Certs.lagda.md
index 35ca740808..bea8132f82 100644
--- a/src/Ledger/Conway/Conformance/Equivalence/Certs.lagda.md
+++ b/src/Ledger/Conway/Conformance/Equivalence/Certs.lagda.md
@@ -160,12 +160,6 @@ instance
                      Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,PRE-CERT⦈ (deposits ⊢conv s')
   PRE-CERTToConf .convⁱ deposits (L.CERT-pre h) = C.CERT-pre h
 
-  POST-CERTToConf : ∀ {Γ s s'}
-                 → L.Deposits × L.Deposits
-                   ⊢ Γ L.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆ⁱ λ deposits _ →
-                     Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,POST-CERT⦈ (deposits ⊢conv s')
-  POST-CERTToConf .convⁱ deposits L.CERT-post = C.CERT-post
-
   DELEGToConf : ∀ {Γ s dcert dcerts s'}
                   (open L.DelegEnv Γ renaming (pparams to pp))
               → CertDeps* pp (dcert ∷ dcerts) ⊢
@@ -183,7 +177,7 @@ instance
                   (open L.CertEnv Γ using (pp))
                 → CertDeps* pp (dcert ∷ dcerts) ⊢
                    Γ L.⊢ s ⇀⦇ dcert ,GOVCERT⦈ s' ⭆ⁱ λ deposits _ →
-                   Γ C.⊢ (deposits .depsᵍ ⊢conv s) ⇀⦇ dcert ,GOVCERT⦈ (updateCertDeps deposits .depsᵍ ⊢conv s')
+                   Γ C.⊢ (getCertDeps* deposits ⊢conv s) ⇀⦇ dcert ,GOVCERT⦈ (getCertDeps* (updateCertDeps deposits) ⊢conv s')
   GOVCERTToConf .convⁱ (regdrep* _ _)     (L.GOVCERT-regdrep h) = C.GOVCERT-regdrep h
   GOVCERTToConf .convⁱ (deregdrep* v _ _) (L.GOVCERT-deregdrep h) = C.GOVCERT-deregdrep (h , v)
   GOVCERTToConf .convⁱ (ccreghot* _ _)    (L.GOVCERT-ccreghot h)  = C.GOVCERT-ccreghot h
@@ -201,23 +195,23 @@ instance
   CERTToConf .convⁱ deposits@(ccreghot* _ _)    (L.CERT-vdel govcert) = C.CERT-vdel (deposits ⊢conv govcert)
   CERTToConf .convⁱ deposits@(reg* _ _)         (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
 
-  CERT-POST-CERTToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
+  CERT*ToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
     → CertDeps* pp dcerts
-      ⊢ RunTraceAndThen L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
-        ⭆ⁱ λ deposits _ → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_
+      ⊢ ReflexiveTransitiveClosure {sts = L._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s'
+        ⭆ⁱ λ deposits _ → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_}
                             Γ (getCertDeps* deposits ⊢conv s) dcerts
                               (getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
-  CERT-POST-CERTToConf .convⁱ deposits (run-[] x) = run-[] ((deposits .depsᵈ , deposits .depsᵍ) ⊢conv x)
-  CERT-POST-CERTToConf .convⁱ deposits (run-∷ x x₁) = run-∷ (deposits ⊢conv x) (updateCertDeps deposits ⊢conv x₁)
+  CERT*ToConf .convⁱ deposits (BS-base Id-nop) = BS-base Id-nop
+  CERT*ToConf .convⁱ deposits (BS-ind x x₁) = BS-ind (deposits ⊢conv x) (updateCertDeps deposits ⊢conv x₁)
 
 
   CERTSToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
     → CertDeps* pp dcerts
-      ⊢ RunTraceAfterAndThen L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
-      ⭆ⁱ λ deposits _ → RunTraceAfterAndThen C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_
+      ⊢ RunTraceAfter L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ Γ s dcerts s'
+      ⭆ⁱ λ deposits _ → RunTraceAfter C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_
                           Γ (getCertDeps* deposits ⊢conv s) dcerts
                             (getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
-  CERTSToConf .convⁱ deposits (run (pre , cert-post)) = run (getCertDeps* deposits ⊢conv pre , deposits ⊢conv cert-post)
+  CERTSToConf .convⁱ deposits (run (pre , cert-trace)) = run (getCertDeps* deposits ⊢conv pre , deposits ⊢conv cert-trace)
 
 -- Converting form Conformance is easier since the deposit tracking disappears.
 instance
@@ -245,21 +239,15 @@ instance
                      Γ L.⊢ (conv s) ⇀⦇ _ ,PRE-CERT⦈ (conv s')
   PRE-CERTFromConf .convⁱ _ (C.CERT-pre h) = L.CERT-pre h
 
-  POST-CERTFromConf : ∀ {Γ s s'}
-                   → Γ C.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆
-                     Γ L.⊢ (conv s) ⇀⦇ _ ,POST-CERT⦈ (conv s')
-  POST-CERTFromConf .convⁱ _ C.CERT-post = L.CERT-post
-
-
-  CERT-POST-CERTFromConf : ∀ {Γ s dcerts s'}
-    → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
-      ⭆ RunTraceAndThen L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ (conv s) dcerts (conv s')
-  CERT-POST-CERTFromConf .convⁱ _ (run-[] x) = run-[] (conv x)
-  CERT-POST-CERTFromConf .convⁱ _ (run-∷ x xs) = run-∷ (conv x) (conv xs)
+  CERT*FromConf : ∀ {Γ s dcerts s'}
+    → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s'
+      ⭆ ReflexiveTransitiveClosure {sts = L._⊢_⇀⦇_,CERT⦈_} Γ (conv s) dcerts (conv s')
+  CERT*FromConf .convⁱ _ (BS-base Id-nop) = BS-base Id-nop
+  CERT*FromConf .convⁱ _ (BS-ind x xs) = BS-ind (conv x) (conv xs)
 
 
   CERTSFromConf : ∀ {Γ s dcerts s'}
-                 → RunTraceAfterAndThen C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s' ⭆
-                   RunTraceAfterAndThen L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ (conv s) dcerts (conv s')
-  CERTSFromConf .convⁱ _ (run (pre , cert-post)) = run ((conv pre) , conv cert-post)
+                 → RunTraceAfter C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_ Γ s dcerts s' ⭆
+                   RunTraceAfter L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ Γ (conv s) dcerts (conv s')
+  CERTSFromConf .convⁱ _ (run (pre , cert-trace)) = run ((conv pre) , conv cert-trace)
 ```
diff --git a/src/Ledger/Conway/Foreign/Cert.agda b/src/Ledger/Conway/Foreign/Cert.agda
index b4b8063aed..74174d1441 100644
--- a/src/Ledger/Conway/Foreign/Cert.agda
+++ b/src/Ledger/Conway/Foreign/Cert.agda
@@ -9,7 +9,7 @@ open import Ledger.Prelude
 open import Ledger.Prelude.Foreign.HSTypes
 
 open import Ledger.Conway.Foreign.HSStructures hiding (CertEnv; DCert) renaming (⟦_,_,_⟧ᶜˢ to ⟦_,_,_⟧ᶜˢ'; CertState to CertState')
-open import Ledger.Conway.Foreign.Certs
+open import Ledger.Conway.Foreign.Certs public
 open import Ledger.Conway.Conformance.Certs.Properties govStructure
   using ( Computational-CERT
         ; Computational-CERTS
@@ -19,9 +19,6 @@ open import Ledger.Conway.Conformance.Certs govStructure
 open Computational
 
 instance
-  HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
-  Conv-CertState = autoConvert CertState
-
   Conv-CertState-CertState' : Convertible CertState CertState'
   Conv-CertState-CertState' .to ⟦ dState , pState , gState ⟧ᶜˢ    = ⟦ to dState , pState , to gState ⟧ᶜˢ'
   Conv-CertState-CertState' .from ⟦ dState , pState , gState ⟧ᶜˢ' = ⟦ from dState , pState , from gState ⟧ᶜˢ
diff --git a/src/Ledger/Conway/Foreign/Certs.agda b/src/Ledger/Conway/Foreign/Certs.agda
index 7a77b77f93..2d29988664 100644
--- a/src/Ledger/Conway/Foreign/Certs.agda
+++ b/src/Ledger/Conway/Foreign/Certs.agda
@@ -11,10 +11,10 @@ open import Ledger.Prelude.Foreign.HSTypes
 
 open import Ledger.Core.Foreign.Address
 open import Ledger.Conway.Foreign.HSStructures renaming (⟦_,_,_⟧ᵈ to ⟦_,_,_⟧ᵈ'; DState to DState'
-                                                              ; ⟦_,_⟧ᵛ to ⟦_,_⟧ᵛ'; GState to GState') hiding (CertEnv)
+                                                              ; ⟦_,_⟧ᵛ to ⟦_,_⟧ᵛ'; GState to GState'; CertState to CertState') hiding (CertEnv)
 open import Ledger.Conway.Foreign.Gov.Core
 open import Ledger.Conway.Foreign.PParams
-open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertEnv)
+open import Ledger.Conway.Conformance.Certs govStructure using (⟦_,_,_,_⟧ᵈ; ⟦_,_,_⟧ᵛ; DState; GState; CertState; CertEnv)
 open import Ledger.Conway.Specification.Certs.Properties.Computational govStructure
   using (Computational-POOL)
 open import Ledger.Conway.Conformance.Certs.Properties govStructure
@@ -80,6 +80,9 @@ instance
     • fieldPrefix "gs"
   Conv-GState = autoConvert GState
 
+  HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
+  Conv-CertState = autoConvert CertState
+
   Conv-DState-DState' : Convertible DState DState'
   Conv-DState-DState' .to ⟦ voteDelegs , stakeDelegs , rewards , deposits ⟧ᵈ = ⟦ voteDelegs , stakeDelegs , stakeDelegs ⟧ᵈ'
   Conv-DState-DState' .from ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ'         = ⟦ voteDelegs , stakeDelegs , stakeDelegs , ∅ ⟧ᵈ
@@ -98,7 +101,7 @@ pool-step = to (compute Computational-POOL)
 
 {-# COMPILE GHC pool-step as poolStep #-}
 
-govcert-step : HsType (CertEnv → GState → DCert → ComputationResult String GState)
+govcert-step : HsType (CertEnv → CertState → DCert → ComputationResult String CertState)
 govcert-step = to (compute Computational-GOVCERT)
 
 {-# COMPILE GHC govcert-step as govCertStep #-}
diff --git a/src/Ledger/Conway/Specification/Certs.lagda.md b/src/Ledger/Conway/Specification/Certs.lagda.md
index a82ca084b8..353c9651b9 100644
--- a/src/Ledger/Conway/Specification/Certs.lagda.md
+++ b/src/Ledger/Conway/Specification/Certs.lagda.md
@@ -361,6 +361,7 @@ private variable
   stᵈ stᵈ' : DState
   stᵍ stᵍ' : GState
   stᵖ stᵖ' : PState
+  stᶜ stᶜ' : CertState
   cc : ℙ Credential
 ```
 -->
@@ -519,23 +520,23 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
 ### Auxiliary <span class="AgdaDatatype">GOVCERT</span> transition system
 
 ```agda
-data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where
+data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
 
   GOVCERT-regdrep :
     ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys ⟧ ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ stᵈ , stᵖ , ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys ⟧ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ , stᵖ , ⟦ dReps , ccKeys ⟧ ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ ⟦ vDelegs ∣^ ❴ vDelegCredential c ❵ ᶜ , sDelegs , rwds ⟧ᵈ , stᵖ , ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys ⟧ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ dReps , ccKeys ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧
+      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys ⟧ ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ stᵈ , stᵖ , ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys ⟧ ⟧
 ```
 
 ## The <span class="AgdaDatatype">CERTS</span> Transition System {#sec:the-certs-transition-system}
@@ -561,9 +562,9 @@ data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState →
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-vdel :
-    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
+    ∙ Γ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
       ────────────────────────────────
-      Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
+      Γ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'
 ```
 
 ### The <span class="AgdaDatatype">PRE-CERT</span> Transition Rule
@@ -607,23 +608,9 @@ data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState →
       ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , ⟦ dReps , ccHotKeys ⟧ ⟧ ⇀⦇ _ ,PRE-CERT⦈ ⟦ ⟦ voteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧ , stᵖ , ⟦ refreshedDReps , ccHotKeys ⟧ ⟧
 ```
 
-### The <span class="AgdaDatatype">POST-CERT</span> Transition Rule
-
-The `POST-CERT`{.AgdaFunction} transition rule is applied at the end of the
-`CERTS`{.AgdaDatatype} rule and it ensures that only valid registered
-`DReps`{.AgdaInductiveConstructor} are included in the final `CertState`{.AgdaRecord}.
-
 ```agda
-data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
-
-  CERT-post :
-    let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
-                         ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
-    in
-      ⟦ e , pp , vs , wdrls , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧ ⇀⦇ _ ,POST-CERT⦈ ⟦ ⟦ voteDelegs ∣^ activeVDelegs , stakeDelegs , rewards ⟧ , stᵖ , stᵍ ⟧
-
 _⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
-_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_
+_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfter _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_
 ```
 
 # References {#references .unnumbered}
diff --git a/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md
index 8e7d613afc..7814543785 100644
--- a/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md
+++ b/src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md
@@ -71,40 +71,39 @@ instance
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
-  Computational-GOVCERT .computeProof ce stᵍ (regdrep c d _) =
+  Computational-GOVCERT .computeProof ce cs (regdrep c d _) =
     let open CertEnv ce; open PParams pp in
-    case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps stᵍ))
-         ⊎ (d ≡ 0 × c ∈ dom (GState.dreps stᵍ)) ¿ of λ where
+    case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps (gState cs)))
+         ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (gState cs))) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof _ stᵍ (deregdrep c _) =
-    let open GState stᵍ in
-    case c ∈? dom dreps of λ where
+  Computational-GOVCERT .computeProof _ cs (deregdrep c _) =
+    case c ∈? dom (GState.dreps (gState cs)) of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce stᵍ (ccreghot c _) =
-    let open CertEnv ce; open GState stᵍ in
-    case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (ccreghot c _) =
+    let open CertEnv ce in
+    case ¿ ((c , nothing) ∉ GState.ccHotKeys (gState cs) ˢ) × c ∈ coldCreds ¿ of λ where
       (yes p) → success (-, GOVCERT-ccreghot p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
-  Computational-GOVCERT .completeness ce stᵍ
+  Computational-GOVCERT .completeness ce cs
     (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
-      ¿ (let open CertEnv ce; open PParams pp; open GState stᵍ in
-        (d ≡ drepDeposit × c ∉ dom dreps) ⊎ (d ≡ 0 × c ∈ dom dreps))
+      ¿ (let open CertEnv ce; open PParams pp in
+        (d ≡ drepDeposit × c ∉ dom (GState.dreps (gState cs))) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (gState cs))))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness _ stᵍ
+  Computational-GOVCERT .completeness _ cs
     (deregdrep c _) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes (c ∈? dom (GState.dreps stᵍ)) p .proj₂ = refl
-  Computational-GOVCERT .completeness ce stᵍ
+    rewrite dec-yes (c ∈? dom (GState.dreps (gState cs))) p .proj₂ = refl
+  Computational-GOVCERT .completeness ce cs
     (ccreghot c _) _ (GOVCERT-ccreghot p)
-    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys stᵍ) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
+    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys (gState cs)) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
 
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
   Computational-CERT .computeProof ce cs dCert
     with computeProof ⟦ CertEnv.pp ce , PState.pools (pState cs) , dom (GState.dreps (gState cs)) ⟧ (dState cs) dCert
-       | computeProof (CertEnv.pp ce) (pState cs) dCert | computeProof ce (gState cs) dCert
+       | computeProof (CertEnv.pp ce) (pState cs) dCert | computeProof ce cs dCert
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
   ... | failure _       | failure _       | success (_ , h) = success (-, CERT-vdel h)
@@ -131,18 +130,17 @@ instance
     with completeness _ _ _ _ h
   ... | refl = refl
   Computational-CERT .completeness ce cs
-    dCert@(regdrep c d an)
-    cs' (CERT-vdel h)
-    with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (regdrep c d an) _ (CERT-vdel (GOVCERT-regdrep p))
+    rewrite dec-yes
+      ¿ (let open CertEnv ce; open PParams pp in
+        (d ≡ drepDeposit × c ∉ dom (GState.dreps (gState cs))) ⊎ (d ≡ 0 × c ∈ dom (GState.dreps (gState cs))))
+      ¿ p .proj₂ = refl
   Computational-CERT .completeness ce cs
-    dCert@(deregdrep c _) cs' (CERT-vdel h)
-    with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (deregdrep c _) _ (CERT-vdel (GOVCERT-deregdrep p))
+    rewrite dec-yes (c ∈? dom (GState.dreps (gState cs))) p .proj₂ = refl
   Computational-CERT .completeness ce cs
-    dCert@(ccreghot c mkh) cs' (CERT-vdel h)
-    with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (ccreghot c _) _ (CERT-vdel (GOVCERT-ccreghot p))
+    rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys (gState cs)) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
 
   Computational-PRE-CERT : Computational _⊢_⇀⦇_,PRE-CERT⦈_ String
   Computational-PRE-CERT .computeProof ce cs _ =
@@ -160,22 +158,6 @@ instance
                 × mapˢ (map₁ RewardAddress.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
         p .proj₂ = refl
 
-  -- POST-CERT has no premises, so computing always succeeds
-  -- with the unique post-state and proof CERT-post.
-  Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
-  Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
-    where
-      dreps : DReps
-      dreps = GState.dreps (gState cs)
-      validVoteDelegs : VoteDelegs
-      validVoteDelegs = (VoteDelegsOf cs) ∣^ ( mapˢ vDelegCredential (dom dreps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
-      cs' : CertState
-      cs' = ⟦ ⟦ validVoteDelegs , StakeDelegsOf cs , RewardsOf cs ⟧ , PStateOf cs , GStateOf cs ⟧
-
-  -- Completeness: the relational proof pins s' to exactly `post`,
-  -- and computeProof returns success at that same state; so refl.
-  Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
-
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it
 ```
diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md
index a4b7277fcc..8a8e5b823f 100644
--- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md
+++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md
@@ -91,7 +91,9 @@ CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
                             ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
                                        (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
 CERT-pov (CERT-pool x) = refl
-CERT-pov (CERT-vdel x) = refl
+CERT-pov (CERT-vdel (GOVCERT-regdrep _)) = refl
+CERT-pov (CERT-vdel (GOVCERT-deregdrep _)) = refl
+CERT-pov (CERT-vdel (GOVCERT-ccreghot _)) = refl
 
 injOn : (wdls : Withdrawals)
         → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
@@ -184,32 +186,6 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
 ```
 -->
 
-**Lemma (`POST-CERT`{.AgdaOperator} rule preserves value).**
-
-*Informally*.
-
-Let `Γ`{.AgdaBound} : `CertEnv`{.AgdaRecord} be a certificate environment, and let
-`s`{.AgdaBound}, `s'`{.AgdaBound} : `CertState`{.AgdaRecord} be certificate states such that
-`s`{.AgdaBound} `⇀⦇`{.AgdaDatatype} \_ `,POST-CERT⦈`{.AgdaDatatype} `s'`{.AgdaBound}.
-Then, the value of `s`{.AgdaBound} is equal to the value of `s'`{.AgdaBound}.
-In other terms,
-
-`getCoin`{.AgdaField} `s`{.AgdaBound} $≡$ `getCoin`{.AgdaField} `s'`{.AgdaBound}.
-
-*Formally*.
-
-```agda
-    POST-CERT-pov : {Γ : CertEnv} {s s' : CertState}
-      → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s'
-      → getCoin s ≡ getCoin s'
-```
-
-*Proof*.
-
-```agda
-    POST-CERT-pov CERT-post = refl
-```
-
 **Lemma (iteration of `CERT`{.AgdaOperator} rule preserves value).**
 
 *Informally*. Let `l`{.AgdaBound} be a list of `DCerts`{.AgdaDatatype}, and let
@@ -222,13 +198,13 @@ Then, the value of `s₁`{.AgdaBound} is equal to the value of `sₙ`{.AgdaBound
 
 ```agda
     sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert}
-      → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ
+      → ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,CERT⦈_} Γ s₁ sigs sₙ
       → getCoin s₁ ≡ getCoin sₙ
 ```
 
 *Proof*.
 
 ```agda
-    sts-pov (run-[] x) = POST-CERT-pov x
-    sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs)
+    sts-pov (BS-base Id-nop) = refl
+    sts-pov (BS-ind x xs) = trans (CERT-pov x) (sts-pov xs)
 ```
diff --git a/src/Ledger/Dijkstra/Foreign/Cert.agda b/src/Ledger/Dijkstra/Foreign/Cert.agda
index c5faf2b6f6..801def1d35 100644
--- a/src/Ledger/Dijkstra/Foreign/Cert.agda
+++ b/src/Ledger/Dijkstra/Foreign/Cert.agda
@@ -17,10 +17,6 @@ open import Ledger.Dijkstra.Specification.Certs.Properties.Computational DummyGo
 
 open Computational
 
-instance
-  HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
-  Conv-CertState = autoConvert CertState
-
 cert-step : HsType (CertEnv → CertState → DCert → ComputationResult String CertState)
 cert-step = to (compute Computational-CERT)
 
diff --git a/src/Ledger/Dijkstra/Foreign/Certs.agda b/src/Ledger/Dijkstra/Foreign/Certs.agda
index 73f42afed7..6cd3734a95 100644
--- a/src/Ledger/Dijkstra/Foreign/Certs.agda
+++ b/src/Ledger/Dijkstra/Foreign/Certs.agda
@@ -59,6 +59,9 @@ instance
     • fieldPrefix "ce"
   Conv-CertEnv = autoConvert CertEnv
 
+  HsTy-CertState = autoHsType CertState ⊣ withConstructor "MkCertState"
+  Conv-CertState = autoConvert CertState
+
 -- Computational step functions
 
 deleg-step : HsType (DelegEnv → DState → DCert → ComputationResult String DState)
@@ -71,7 +74,7 @@ pool-step = to (compute Computational-POOL)
 
 {-# COMPILE GHC pool-step as poolStep #-}
 
-govcert-step : HsType (GovCertEnv → GState → DCert → ComputationResult String GState)
+govcert-step : HsType (GovCertEnv → CertState → DCert → ComputationResult String CertState)
 govcert-step = to (compute Computational-GOVCERT)
 
 {-# COMPILE GHC govcert-step as govCertStep #-}
diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md
index a4100f60ec..67e62bfd96 100644
--- a/src/Ledger/Dijkstra/Specification/Certs.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Certs.lagda.md
@@ -302,6 +302,8 @@ private variable
   retiring               : Retiring
   A                      : Type
   deposits deposits'     : A ⇀ Coin
+  depositsᵍ depositsᵍ'    : Credential ⇀ Coin
+  depositsᵈ depositsᵈ'    : Credential ⇀ Coin
 
   an          : Anchor
   Γ           : CertEnv
@@ -321,6 +323,7 @@ private variable
   stᵈ stᵈ' : DState
   stᵍ stᵍ' : GState
   stᵖ stᵖ' : PState
+  stᶜ stᶜ' : CertState
   cc : ℙ Credential
 ```
 -->
@@ -448,24 +451,24 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type wh
 ## `GOVCERT`{.AgdaDatatype} Transition System
 
 ```agda
-data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type where
+data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → CertState → DCert → CertState → Type where
 
   GOVCERT-regdrep :
     ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
       ────────────────────────────────
-      ⟦ e , pp , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , deposits ∪⁺ ❴ c , d ❵ ⟧
+      ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , depositsᵍ ⟧ ⟧ ⇀⦇ regdrep c d an ,GOVCERT⦈ ⟦ stᵈ , stᵖ , ⟦ ❴ c , e + pp .drepActivity ❵ ∪ˡ dReps , ccKeys , depositsᵍ ∪⁺ ❴ c , d ❵ ⟧ ⟧
 
   GOVCERT-deregdrep :
     ∙ c ∈ dom dReps
-    ∙ (c , d) ∈ deposits
+    ∙ (c , d) ∈ depositsᵍ
       ────────────────────────────────
-      ⟦ e , pp , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , deposits ∣ ❴ c ❵ ᶜ ⟧
+      ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ vDelegs , sDelegs , rwds , depositsᵈ ⟧ , stᵖ , ⟦ dReps , ccKeys , depositsᵍ ⟧ ⟧ ⇀⦇ deregdrep c d ,GOVCERT⦈ ⟦ ⟦ vDelegs ∣^ ❴ vDelegCredential c ❵ ᶜ , sDelegs , rwds , depositsᵈ ⟧ , stᵖ , ⟦ dReps ∣ ❴ c ❵ ᶜ , ccKeys , depositsᵍ ∣ ❴ c ❵ ᶜ ⟧ ⟧
 
   GOVCERT-ccreghot :
     ∙ (c , nothing) ∉ ccKeys
     ∙ c ∈ cc
       ────────────────────────────────
-      ⟦ e , pp , cc ⟧ ⊢ ⟦ dReps , ccKeys , deposits ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , deposits ⟧
+      ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , ⟦ dReps , ccKeys , depositsᵍ ⟧ ⟧ ⇀⦇ ccreghot c mc ,GOVCERT⦈ ⟦ stᵈ , stᵖ , ⟦ dReps , ❴ c , mc ❵ ∪ˡ ccKeys , depositsᵍ ⟧ ⟧
 ```
 
 # `CERT`{.AgdaDatatype} Transition System
@@ -484,9 +487,9 @@ data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState →
       ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧
 
   CERT-gov :
-    ∙ ⟦ e , pp , cc ⟧ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
+    ∙ ⟦ e , pp , cc ⟧ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
       ────────────────────────────────
-      ⟦ e , pp , cc ⟧ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧
+      ⟦ e , pp , cc ⟧ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'
 ```
 
 # `CERTS`{.AgdaDatatype} Transition System
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md
index e2f64e5833..fdf678590d 100644
--- a/src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md
@@ -72,35 +72,35 @@ instance
   Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
 
   Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
-  Computational-GOVCERT .computeProof ce gs (regdrep c d _) =
-    case ¿ d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs)
-         ⊎ d ≡ 0 × c ∈ dom (DRepsOf gs) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (regdrep c d _) =
+    case ¿ d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf cs)
+         ⊎ d ≡ 0 × c ∈ dom (DRepsOf cs) ¿ of λ where
       (yes p) → success (-, GOVCERT-regdrep p)
       (no ¬p) → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (deregdrep c d) =
-    case ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈  (DepositsOf gs) ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (deregdrep c d) =
+    case ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈  (DepositsOf (GStateOf cs)) ¿ of λ where
       (yes p) → success (-, GOVCERT-deregdrep p)
       (no ¬p)  → failure (genErrors ¬p)
-  Computational-GOVCERT .computeProof ce gs (ccreghot c _) =
-    case ¿ ((c , nothing) ∉ CCHotKeysOf gs ˢ) × c ∈ ColdCredentialsOf ce ¿ of λ where
+  Computational-GOVCERT .computeProof ce cs (ccreghot c _) =
+    case ¿ ((c , nothing) ∉ CCHotKeysOf cs ˢ) × c ∈ ColdCredentialsOf ce ¿ of λ where
       (yes p) → success (-, GOVCERT-ccreghot p)
       (no ¬p) → failure (genErrors ¬p)
   Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
-  Computational-GOVCERT .completeness ce gs (regdrep c d _) _ (GOVCERT-regdrep p)
+  Computational-GOVCERT .completeness ce cs (regdrep c d _) _ (GOVCERT-regdrep p)
     rewrite dec-yes
-      ¿  (d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs))
-         ⊎ (d ≡ 0 × c ∈ dom (DRepsOf gs))
+      ¿  (d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf cs))
+         ⊎ (d ≡ 0 × c ∈ dom (DRepsOf cs))
       ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness _ gs (deregdrep c d) _ (GOVCERT-deregdrep p)
-    rewrite dec-yes ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈ (DepositsOf gs) ¿ p .proj₂ = refl
-  Computational-GOVCERT .completeness ce gs (ccreghot c _) _ (GOVCERT-ccreghot p)
-    rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf gs ˢ × c ∈ ColdCredentialsOf ce ¿ p .proj₂ = refl
+  Computational-GOVCERT .completeness _ cs (deregdrep c d) _ (GOVCERT-deregdrep p)
+    rewrite dec-yes ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈ (DepositsOf (GStateOf cs)) ¿ p .proj₂ = refl
+  Computational-GOVCERT .completeness ce cs (ccreghot c _) _ (GOVCERT-ccreghot p)
+    rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf cs ˢ × c ∈ ColdCredentialsOf ce ¿ p .proj₂ = refl
 
   Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
   Computational-CERT .computeProof ce cs dCert
     with computeProof ⟦ PParamsOf ce , PoolsOf cs , dom (DRepsOf cs) ⟧ (DStateOf cs) dCert
          | computeProof (PParamsOf ce) (PStateOf cs) dCert
-         | computeProof ⟦ EpochOf ce , PParamsOf ce , ColdCredentialsOf ce ⟧ (GStateOf cs) dCert
+         | computeProof ⟦ EpochOf ce , PParamsOf ce , ColdCredentialsOf ce ⟧ cs dCert
 
   ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
   ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
@@ -127,17 +127,17 @@ instance
     with completeness _ _ _ _ h
   ... | refl = refl
   Computational-CERT .completeness Γ cs
-    dCert@(regdrep c _ _) cs' (CERT-gov h)
-    with computeProof ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (regdrep c d an) _ (CERT-gov (GOVCERT-regdrep p))
+    rewrite dec-yes
+      ¿  (d ≡ PParams.drepDeposit (PParamsOf Γ) × c ∉ dom (DRepsOf cs))
+         ⊎ (d ≡ 0 × c ∈ dom (DRepsOf cs))
+      ¿ p .proj₂ = refl
   Computational-CERT .completeness Γ cs
-    dCert@(deregdrep c _) cs' (CERT-gov h)
-    with computeProof ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (deregdrep c d) _ (CERT-gov (GOVCERT-deregdrep p))
+    rewrite dec-yes ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈ (DepositsOf (GStateOf cs)) ¿ p .proj₂ = refl
   Computational-CERT .completeness Γ cs
-    dCert@(ccreghot c mkh) cs' (CERT-gov h)
-    with computeProof ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧ (CertState.gState cs) dCert | completeness _ _ _ _ h
-  ... | success _ | refl = refl
+    (ccreghot c mc) _ (CERT-gov (GOVCERT-ccreghot p))
+    rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf cs ˢ × c ∈ ColdCredentialsOf Γ ¿ p .proj₂ = refl
 
 Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
 Computational-CERTS = it
diff --git a/src/Ledger/Dijkstra/Specification/Entities.lagda.md b/src/Ledger/Dijkstra/Specification/Entities.lagda.md
index af40a8bb8f..f0876ec7dc 100644
--- a/src/Ledger/Dijkstra/Specification/Entities.lagda.md
+++ b/src/Ledger/Dijkstra/Specification/Entities.lagda.md
@@ -147,8 +147,6 @@ data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx
   SUBENTITIES :
     let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub))
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
-        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
-                               ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
 
         withdrawals               = WithdrawalsOf txSub
         withdrawalsCredentials    = mapˢ stake (dom withdrawals)
@@ -169,7 +167,7 @@ data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx
     ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
     ∙ directDepositsCredentials ⊆ dom rewards'
       ────────────────────────────────
-      ⟦ e , pp , cc , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+      ⟦ e , pp , cc , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
 ```
 
 ```agda
@@ -178,8 +176,6 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce
   ENTITIES :
     let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
         refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
-        activeVDelegs   = mapˢ vDelegCredential (dom (DRepsOf gState'))
-                               ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
 
         withdrawalsSubTxs          = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
         withdrawals                = WithdrawalsOf txTop
@@ -209,5 +205,5 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce
     ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
     ∙ directDepositsCredentials ⊆ dom rewards'
       ────────────────────────────────
-      ⟦ e , pp , cc , legacyMode , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txTop ,ENTITIES⦈ ⟦ ⟦ voteDelegs' ∣^ activeVDelegs , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
+      ⟦ e , pp , cc , legacyMode , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txTop ,ENTITIES⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
 ```