{-# OPTIONS --safe #-} open import Ledger.Conway.Abstract open import Ledger.Conway.Transaction module Ledger.Conway.GovernanceActions.Properties.ChangePPGroup (txs : _) (open TransactionStructure txs) where open import Ledger.Prelude instance _ : IsSet TxBody GovProposal _ = record { toSet = fromList ∘ TxBody.txprop } ChangePPHasGroup : {tx : Tx} {p : GovProposal} (pu : PParamsUpdate) → p ∈ Tx.body tx → p .GovProposal.action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.GovernanceActions.html#898}{\htmlId{453}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.GovernanceActions.Properties.ChangePPGroup.html#386}{\htmlId{469}{\htmlClass{Bound}{\text{pu}}}}\, \end{pmatrix}$ → Type ChangePPHasGroup pu _ _ = updateGroups pu ≢ ∅