NoPropSameDReps

{-# OPTIONS --safe #-}

open import Ledger.Conway.Transaction
open import Ledger.Conway.Abstract

module Ledger.Conway.Epoch.Properties.NoPropSameDReps
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Epoch txs abs
open import Ledger.Conway.Gov txs
open import Ledger.Prelude
open import Ledger.Conway.Properties txs abs

- *Informally*. If there are no governance proposals in the `GovState`{.AgdaFunction} of , then the `activeDReps`{.AgdaField} of in `Epoch`{.AgdaDatatype} are the same as the `activeDReps`{.AgdaField} of in the next epoch. - *Formally*.

prop≡∅⇒activeDReps-const : Epoch → (es es' : NewEpochState) → Type
prop≡∅⇒activeDReps-const e es es' =
  GovStateOf es ≡ [] → activeDReps e es ≡ᵉ activeDReps (sucᵉ e) es'

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).