{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

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

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


voteDelegsVDeleg :  DState → Type
voteDelegsVDeleg d = range (VoteDelegsOf d) ⊆ mapˢ vDelegCredential (dom (VoteDelegsOf d))