refactor: remove claim twice rule as it should not be possible

certora/helpers/MerkleTree.sol

@@ -27,13 +27,14 @@ contract MerkleTree {
     /* STORAGE */
 
     // The tree has no root because every node (and the nodes underneath) form a Merkle tree.
+    // We use bytes32 as keys of the mapping so that leaves can have an identifier that is the hash of the address and the reward token.
+    // This ensures that the same pair of address and reward token does not appear twice as a leaf in the tree.
+    // For internal nodes the key is left arbitrary, so that the certificate generation can choose freely any bytes32 value (that is not already used).
     mapping(bytes32 => Node) internal tree;
 
     /* MAIN FUNCTIONS */
 
     function newLeaf(Leaf memory leaf) public {
-        // The following identifier is used as the key to create a new leaf.
-        // This ensures that the same pair of address and reward does not appear twice in the tree.
         bytes32 id = keccak256(abi.encode(leaf.addr, leaf.reward));
         Node storage node = tree[id];
         require(id != 0, "id is the zero bytes");

certora/specs/UniversalRewardsDistributor.spec

@@ -48,23 +48,6 @@ rule increasingClaimedAmounts(address account, address reward, uint256 claimable
     assert claimable > claimed;
 }
 
-// Check that claiming twice is equivalent to claiming once with the last amount.
-rule claimTwice(address account, address reward, uint256 claim1, uint256 claim2) {
-    storage initStorage = lastStorage;
-
-    bytes32[] proof1; bytes32[] proof2;
-    claim(account, reward, claim1, proof1);
-    claim(account, reward, claim2, proof2);
-    assert claim2 >= claim1;
-
-    storage afterBothStorage = lastStorage;
-
-    bytes32[] proof3;
-    claim(account, reward, claim2, proof3) at initStorage;
-
-    assert lastStorage == afterBothStorage;
-}
-
 // Check that the transferred amount is equal to the claimed amount minus the previous claimed amount.
 rule transferredTokens(address account, address reward, uint256 claimable, bytes32[] proof) {
     // Assume that the rewards distributor itself is not receiving the tokens, to simplify this rule.