{-# OPTIONS --safe #-}

open import Ledger.Conway.Gov.Base

module Ledger.Conway.Certs.Properties.VoteDelegsVDeleg (gs : _) (open GovStructure gs) where

open import Ledger.Conway.Certs gs
open import Ledger.Prelude
open import Ledger.Conway.Gov.Actions gs


voteDelegsVDeleg :  DState → Type
voteDelegsVDeleg d = range (voteDelegsOf d) ⊆ mapˢ (credVoter DRep) (dom (voteDelegsOf d))