Prove that GA deposits match current proposals

[WhatisRT]

We should prove that the following property is an invariant, i.e. that if it holds for some state it also holds when we successfully apply a block to that state.

filterˢ isGADeposit (dom (UTxOState.deposits utxoSt))
    ≡ fromList (map (λ where (id , _) → GovActionDeposit id) govSt)

Where isGADeposit is a decision procedure whether a deposit was constructed via the GovActionDeposit constructor.