diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 002dde0d..eecd3ee2 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -226,6 +226,12 @@ info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
   mem_omega  -- by default, process all hyps
 
 /--
+warning: unused variable `h'`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+---
+warning: unused variable `hab`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+---
 info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
 [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1
 [simp_mem.info] Adding omega facts from hypotheses
@@ -244,6 +250,9 @@ example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by
 
 
 /--
+warning: unused variable `h'`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+---
 warning: unused variable `hab`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 ---