diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
index 93fc894b..83fe5722 100644
--- a/certora/specs/Health.spec
+++ b/certora/specs/Health.spec
@@ -78,9 +78,12 @@ filtered {
     assert !priceChanged => stillHealthy;
 }
 
-rule stayHealthy_liquidate(env e)
-{
-    MorphoHarness.MarketParams marketParams;
+// The general case of liquidate for the stayHealthy rule
+//   - the user checked is not the borrower,
+//   - the market of the liquidation is the market of the user,
+//   - there is still some borrow on the market after liquidation,
+//   - there was no bad debt realization.
+rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
     MorphoHarness.Id id = libId(marketParams);
     address user;
 
@@ -94,22 +97,14 @@ rule stayHealthy_liquidate(env e)
     require lastUpdate(id) == e.block.timestamp;
 
     priceChanged = false;
-
-    MorphoHarness.MarketParams marketParams2;
-    address borrower;
-    uint256 seizedAssets;
-    uint256 repaidShares;
-    bytes data;
-    require marketParams2 == marketParams;
-
-    liquidate(e, marketParams2, borrower, seizedAssets, 0, data);
+    liquidate(e, marketParams, borrower, seizedAssets, 0, data);
     require !priceChanged;
+
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
-
-    // the case where not everything was repaid
+    // Handle the case where not everything was repaid.
     require totalBorrowAssets(id) > 0;
-    // user has collateral left
+    // Handle the case where the user has some collateral left.
     require collateral(id, borrower) > 0;
 
     assert user != borrower;
@@ -117,9 +112,6 @@ rule stayHealthy_liquidate(env e)
     assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
 
     bool stillHealthy = isHealthy(marketParams, user);
-    require !priceChanged;
-
-    // assert !priceChanged => stillHealthy;
     assert stillHealthy;
 }