NoPropSameDReps
Claim (DReps unchanged if no gov proposals).
Informally.
If es
is a NewEpochState
, and if the
GovState
of es
contains no governance proposals,
then the set of activeDReps
of es
in
Epoch
e
is equal to the set of
activeDReps
of es
in the next epoch.
Formally.
prop≡∅⇒activeDReps-const : Epoch → NewEpochState → Type prop≡∅⇒activeDReps-const e es = GovStateOf es ≡ [] → activeDReps e es ≡ᵉ activeDReps (sucᵉ e) es
Proof. (coming soon)