{-# OPTIONS --safe #-}

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

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

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Prelude
open import Ledger.Conway.Specification.Properties txs abs


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