diff --git a/lean/Spa/Transformation/Licm.lean b/lean/Spa/Transformation/Licm.lean
index 1774bb4..63f7e98 100644
--- a/lean/Spa/Transformation/Licm.lean
+++ b/lean/Spa/Transformation/Licm.lean
@@ -47,17 +47,17 @@ structure Candidate where
 `enclosing` carries the current loop's tag and body id-set, or `none` outside any
 loop (in which case assignments are skipped — only in-loop assignments are
 candidates). -/
-def collectCandidates :
-    Option (NodeId × List NodeId) → Stmt.Tagged NodeId → List Candidate
-  | enc, .basic _ bs =>
+def collectCandidates (enc : Option (NodeId × List NodeId)) :
+    Stmt.Tagged NodeId → List Candidate
+  | .basic _ bs =>
       match bs, enc with
       | .assign t _ e, some (loopId, bodyIds) =>
           [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
              rhsVars := e.erase.vars.sort (· ≤ ·) }]
       | _, _ => []
-  | enc, .andThen _ a b => collectCandidates enc a ++ collectCandidates enc b
-  | enc, .ifElse _ _ a b => collectCandidates enc a ++ collectCandidates enc b
-  | _, .whileLoop loopT _ body =>
+  | .andThen _ a b => collectCandidates enc a ++ collectCandidates enc b
+  | .ifElse _ _ a b => collectCandidates enc a ++ collectCandidates enc b
+  | .whileLoop loopT _ body =>
       collectCandidates (some (loopT, body.subtreeIds)) body
 
 /-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/