diff --git a/src/Interface/STS.agda b/src/Interface/STS.agda
index 1e1641899..cbe268b17 100644
--- a/src/Interface/STS.agda
+++ b/src/Interface/STS.agda
@@ -53,21 +53,6 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧
         ───────────────────────────────────────
         Γ ⊢ s  ⇀⟦ sig ∷ sigs ⟧* s''
 
-module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where
-  data _⊢_⇀⟦_⟧*ʳ_ : C → S → List Sig → S → Type where
-
-    BS-baseʳ :
-      Γ ⊢ s ⇀⟦ _ ⟧ᵇ s'
-      ───────────────────────────────────────
-      Γ ⊢ s ⇀⟦ [] ⟧*ʳ s'
-
-    BS-indʳ :
-        Γ ⊢ s' ⇀⟦ sigs ⟧*ʳ s''
-      → Γ ⊢ s  ⇀⟦ sig  ⟧   s'
-        ───────────────────────────────────────
-        Γ ⊢ s  ⇀⟦ sigs ∷ʳ sig ⟧*ʳ s''
-
-
 module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type) where
   data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Type where
 
@@ -116,7 +101,7 @@ ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
       case SS-total of λ where
         (s' , Ps') → map₂′ (BS-ind Ps') $ helper SS-total
 
-ReflexiveTransitiveClosureᵣᵇ = _⊢_⇀⟦_⟧*ʳ_
+-- with a given base case
 ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_
 ReflexiveTransitiveClosureᵇ  = _⊢_⇀⟦_⟧*_
 
diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
index d359c23cc..aa8c4c497 100644
--- a/src/Ledger/Certs.lagda
+++ b/src/Ledger/Certs.lagda
@@ -264,42 +264,41 @@ constitutional committee.
 \end{itemize}
 
 \begin{figure*}[h]
-\begin{AgdaSuppressSpace}
+\begin{AgdaMultiCode}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,DELEG⦈_     : DelegEnv → DState → DCert → DState → Type
+    _⊢_⇀⦇_,DELEG⦈_     : DelegEnv → DState → DCert → DState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,POOL⦈_      : PoolEnv → PState → DCert → PState → Type
+    _⊢_⇀⦇_,POOL⦈_      : PoolEnv → PState → DCert → PState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv → GState → DCert → GState → Type
+    _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv → GState → DCert → GState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,CERT⦈_      : CertEnv → CertState → DCert → CertState → Type
+    _⊢_⇀⦇_,CERT⦈_      : CertEnv → CertState → DCert → CertState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv → CertState → ⊤ → CertState → Type
-\end{code}
-\begin{code}
-_⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
+    _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv → CertState → ⊤ → CertState → Type
+
+_⊢_⇀⦇_,CERTS⦈_       : CertEnv → CertState → List DCert → CertState → Type
 _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,CERT⦈_
 \end{code}
-\end{AgdaSuppressSpace}
+\end{AgdaMultiCode}
 \caption{Types for the transition systems relating to certificates}
 \label{fig:sts:certs-types}
 \end{figure*}
@@ -318,15 +317,15 @@ data _⊢_⇀⦇_,DELEG⦈_ where
         fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
-        ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mkh d ,DELEG⦈
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ
+        ⇀⦇ delegate c mv mkh d ,DELEG⦈
         ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
 
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢  ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
-                          ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
+        ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary DELEG transition system}
@@ -430,7 +429,8 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     refresh          = mapPartial getDRepVote (fromList vs)
     refreshedDReps   = mapValueRestricted (const (e + drepActivity)) dReps refresh
     wdrlCreds        = mapˢ stake (dom wdrls)
-    validVoteDelegs  = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
+    validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
+                                        ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
     in
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
diff --git a/src/Ledger/Certs/Properties.agda b/src/Ledger/Certs/Properties.agda
index 7be651885..85a1d5537 100644
--- a/src/Ledger/Certs/Properties.agda
+++ b/src/Ledger/Certs/Properties.agda
@@ -221,7 +221,11 @@ module CERTSpov  (Γ : CertEnv)
   injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
     cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
 
-  module _
+  CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ
+  CERTS-pov (BS-base Id-nop) = refl
+  CERTS-pov (BS-ind x xs) = trans (CERT-pov x) (CERTS-pov xs)
+
+  module CERTBASEpov
     -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
     ( sumConstZero    :  {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
     ( res-decomp      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
@@ -281,9 +285,5 @@ module CERTSpov  (Γ : CertEnv)
           getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls
             ∎
 
-    CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ
-    CERTS-pov (BS-base Id-nop) = refl
-    CERTS-pov (BS-ind x xs) = trans (CERT-pov x) (CERTS-pov xs)
-
 -- TODO: Prove the following property.
 -- range vDelegs ⊆ map (credVoter DRep) (dom DReps)
diff --git a/src/Ledger/Ledger.lagda b/src/Ledger/Ledger.lagda
index 94c7d26af..8b2768e87 100644
--- a/src/Ledger/Ledger.lagda
+++ b/src/Ledger/Ledger.lagda
@@ -80,7 +80,7 @@ private variable
   s s' s'' : LState
   utxoSt' : UTxOState
   govSt' : GovState
-  certState₀ certState₁ certState' : CertState
+  certState' certState'' : CertState
   tx : Tx
 \end{code}
 
@@ -111,11 +111,11 @@ data
                  Γᶜ = ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ  in
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
-    ∙  Γᶜ ⊢ certState ⇀⦇ _ ,CERTBASE⦈ certState₁
-    ∙  Γᶜ ⊢ certState₁ ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
+    ∙  Γᶜ ⊢ certState ⇀⦇ _ ,CERTBASE⦈ certState'
+    ∙  Γᶜ ⊢ certState' ⇀⦇ txcerts ,CERTS⦈ certState''
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState'' ⟧ᵍ ⊢ govSt |ᵒ certState'' ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
-       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ
+       Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState'' ⟧ˡ
 \end{code}
 \begin{NoConway}
 \begin{code}
diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda
index 49fe5db47..e07287d67 100644
--- a/src/Ledger/Ledger/Properties.agda
+++ b/src/Ledger/Ledger/Properties.agda
@@ -73,9 +73,9 @@ instance
       computeProof = case isValid ≟ true of λ where
         (yes p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
-          (certState₁ , certStep) ← computeCert certΓ certState _
-          (certState' , certStep') ← computeCerts certΓ certState₁ txcerts
-          (govSt'  , govStep)  ← computeGov (govΓ certState') (govSt |ᵒ certState') (txgov txb)
+          (certState' , certStep) ← computeCert certΓ certState _
+          (certState'' , certStep') ← computeCerts certΓ certState' txcerts
+          (govSt'  , govStep)  ← computeGov (govΓ certState'') (govSt |ᵒ certState'') (txgov txb)
           success (_ , LEDGER-V⋯ p utxoStep certStep certStep' govStep)
         (no ¬p) → do
           (utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
@@ -89,12 +89,12 @@ instance
         with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
       ... | success (utxoSt' , _) | refl
         with computeCert certΓ certState _ | complete certΓ _ _ _ certStep
-      ... | success (certState₁ , _) | refl
-        with computeCerts certΓ certState₁ txcerts | complete certΓ _ _ _ certStep'
       ... | success (certState' , _) | refl
-        with computeGov (govΓ certState') (govSt |ᵒ certState') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certState') _ _ _ govStep
+        with computeCerts certΓ certState' txcerts | complete certΓ _ _ _ certStep'
+      ... | success (certState'' , _) | refl
+        with computeGov (govΓ certState'') (govSt |ᵒ certState'') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certState'') _ _ _ govStep
       ... | success (govSt' , _) | refl = refl
-      completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
+      completeness ⟦ utxoSt' , govSt' , certState'' ⟧ˡ (LEDGER-I⋯ i utxoStep)
         with isValid ≟ true
       ... | yes refl = case i of λ ()
       ... | no ¬v
@@ -138,34 +138,35 @@ module _
   LEDGER-pov
     {s = ⟦ utxoSt , govSt , ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⟧ˡ}
     {s' = ⟦ utxoSt' , govSt' , ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ ⟧ˡ}
-    h (LEDGER-V {s = s} {utxoSt' = utxoSt'} {certState₁} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , h'' , _ )) =
+    h (LEDGER-V {s = s} {utxoSt' = utxoSt'} {certState'} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , h'' , _ )) =
       let
         open ≡-Reasoning
         open LState s using (certState)
         open CERTSpov ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ indexedSumᵛ'-∪
-        certState' = ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
+        open CERTBASEpov sumConstZero  res-decomp getCoin-cong ≡ᵉ-getCoinˢ r
+        certState'' = ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
         zeroMap    = constMap (mapˢ RwdAddr.stake (dom txwdrls)) 0
       in
       begin
         getCoin utxoSt + getCoin certState
           ≡⟨ cong (getCoin utxoSt +_)
              ( begin rewardsBalance stᵈ
-                 ≡⟨ CERTBASE-pov sumConstZero  res-decomp getCoin-cong ≡ᵉ-getCoinˢ r  h' ⟩
-               getCoin certState₁ + getCoin txwdrls
-                 ≡⟨ cong (_+ getCoin txwdrls) (CERTS-pov sumConstZero  res-decomp getCoin-cong ≡ᵉ-getCoinˢ r h'') ⟩
-               rewardsBalance (CertState.dState certState') + getCoin txwdrls
+                 ≡⟨ CERTBASE-pov h' ⟩
+               getCoin certState' + getCoin txwdrls
+                 ≡⟨ cong (_+ getCoin txwdrls) (CERTS-pov h'') ⟩
+               rewardsBalance (CertState.dState certState'') + getCoin txwdrls
                  ∎
              )
            ⟩
-        getCoin utxoSt + (getCoin certState' + getCoin txwdrls)
-          ≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState' + φ (getCoin txwdrls , u))) valid ⟩
-        getCoin utxoSt + (getCoin certState' + φ (getCoin txwdrls , isValid))
-          ≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState') _) ⟩
-        getCoin utxoSt + (φ (getCoin txwdrls , isValid) + getCoin certState')
-          ≡˘⟨ +-assoc (getCoin utxoSt) (φ (getCoin txwdrls , isValid)) (getCoin certState') ⟩
-        getCoin utxoSt + φ (getCoin txwdrls , isValid) + getCoin certState'
-          ≡⟨ cong (_+ getCoin certState') (pov h st) ⟩
-        getCoin utxoSt' + getCoin certState'
+        getCoin utxoSt + (getCoin certState'' + getCoin txwdrls)
+          ≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState'' + φ (getCoin txwdrls , u))) valid ⟩
+        getCoin utxoSt + (getCoin certState'' + φ (getCoin txwdrls , isValid))
+          ≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState'') _) ⟩
+        getCoin utxoSt + (φ (getCoin txwdrls , isValid) + getCoin certState'')
+          ≡˘⟨ +-assoc (getCoin utxoSt) (φ (getCoin txwdrls , isValid)) (getCoin certState'') ⟩
+        getCoin utxoSt + φ (getCoin txwdrls , isValid) + getCoin certState''
+          ≡⟨ cong (_+ getCoin certState'') (pov h st) ⟩
+        getCoin utxoSt' + getCoin certState''
           ∎
 
   LEDGER-pov  s@{s = ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , ⟦ dState , pState , gState ⟧ᶜˢ ⟧ˡ}
@@ -252,7 +253,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
       → (_⊢_⇀⟦_⟧ᵢ*'_ 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 (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
 
@@ -544,7 +545,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' , certState' ⟧ˡ}
+                          , 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) ⟩
@@ -553,8 +554,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')))
+        ≈˘⟨ |ᵒ-GAs-pres 0 govSt certState'' ⟩
+      fromList (dpMap (updateGovStates (txgov txb) 0 (govSt |ᵒ certState'')))
         ≡˘⟨ cong (fromList ∘ dpMap ) (STS→GovSt≡ utxosts tx-valid) ⟩
       fromList (dpMap govSt') ∎