diff --git a/certora/specs/RevertsERC20.spec b/certora/specs/RevertsERC20.spec
index 0d4e980..782f007 100644
--- a/certora/specs/RevertsERC20.spec
+++ b/certora/specs/RevertsERC20.spec
@@ -17,7 +17,7 @@ rule transferRevertConditions(env e, address to, uint256 amount) {
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require delegatee(e.msg.sender) != 0 => senderVotingPowerBefore >= balanceOfSenderBefore;
 
-    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply.
+    // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require e.msg.sender != 0 => amount <= balanceOfSenderBefore => delegatee(to) != delegatee(e.msg.sender) => recipientVotingPowerBefore + amount <= totalSupply();
 
     transfer@withrevert(e, to, amount);
@@ -33,7 +33,7 @@ rule transferFromRevertConditions(env e, address from, address to, uint256 amoun
 
     // Safe require as it is verified in delegatedLTEqDelegateeVP.
     require delegatee(from) != 0 => holderVotingPowerBefore >= balanceOfHolderBefore;
-    // Safe require that follows from sumOfTwoDelegatedVPLTEqTotalVP() and totalSupplyIsSumOfVirtualVotingPower() and rule updatedDelegatedVPLTEqTotalSupply
+    // Safe require as it proven in rule updatedDelegatedVPLTEqTotalSupply.
     require from != 0 => amount <= balanceOfHolderBefore => delegatee(to) != delegatee(from) => recipientVotingPowerBefore + amount <= totalSupply();
 
     transferFrom@withrevert(e, from, to, amount);