diff --git a/projects/smt-axioms/ProgramVC/Wasm/Lang.lean b/projects/smt-axioms/ProgramVC/Wasm/Lang.lean
index 3a461736..6524aad3 100644
--- a/projects/smt-axioms/ProgramVC/Wasm/Lang.lean
+++ b/projects/smt-axioms/ProgramVC/Wasm/Lang.lean
@@ -175,7 +175,7 @@ theorem pop32_eq {rs rs' : List Val} {c : BitVec 32} (h : pop32 rs = some (c, rs
   · cases h
 
 theorem sizeOf_list_pos {α : Type} [SizeOf α] (l : List α) : 0 < sizeOf l := by
-  cases l <;> simp <;> omega
+  cases l <;> (simp <;> omega)
 
 /-- The little-endian word at byte address `a` of the memory bytes `B`. -/
 def ld32 (B : ByteArray) (a : Nat) : BitVec 32 := BitVec.ofNat 32 (leNat (bytesAt B ⟨a, 4⟩))
@@ -353,7 +353,7 @@ theorem havoc_locals_getElem? (f : Frame) (xs : List (Nat × IntType)) (w : Nat
     · subst hj
       cases t <;> simp [havoc, havocLocals, List.lookup, List.getElem?_set, hlen]
     · have hb : (j == k) = false := by simpa using hj
-      cases t <;> simp [havoc, havocLocals, List.lookup, hb, List.getElem?_set, Ne.symm hj, ih]
+      cases t <;> simp [havoc, havocLocals, List.lookup, hb, Ne.symm hj, ih]
 
 /-- Positionwise form of `LocsOk`. -/
 theorem locsOk_getElem? {xs : List (Nat × IntType)} :
diff --git a/projects/smt-axioms/SmtVc/Reify.lean b/projects/smt-axioms/SmtVc/Reify.lean
index b48a677e..5c234602 100644
--- a/projects/smt-axioms/SmtVc/Reify.lean
+++ b/projects/smt-axioms/SmtVc/Reify.lean
@@ -278,8 +278,8 @@ where
       return .rotr k (← reifyBv r w a)
     | (``cond, #[_, c, a, b]) => return .ite (← reifyBool r c) (← reifyBv r w a) (← reifyBv r w b)
     | (``HAppend.hAppend, #[_, _, _, _, a, b]) =>
-      let ⟨m, a'⟩ ← bvOf r a
-      let ⟨n, b'⟩ ← bvOf r b
+      let ⟨_m, a'⟩ ← bvOf r a
+      let ⟨_n, b'⟩ ← bvOf r b
       castW (Term.concat a' b')
     | (``BitVec.extractLsb', #[_, lo, len, a]) =>
       let some lo ← natLit? lo | fail m!"non-literal extract index"