chore: fix unused hp

Author: luisacicolini

src/Init/Data/BitVec/Bitblast.lean

@@ -3270,8 +3270,6 @@ theorem addRecAux_extractAndExtendPopulateAux_le_of_le {x : BitVec w} (hn : n 
       · have := Nat.lt_two_pow_self (n := w + 1 + 1)
         omega
 
-
-
 theorem addRecAux_extractAndExtendPopulateAux_le_of_le_of_lt {x : BitVec (w + 1)} (hn : n ≤ w) :
     ((extractAndExtendPopulate w x).addRecAux n 0#w).toNat ≤ n := by
   induction n

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean

@@ -181,7 +181,7 @@ theorem denote_blastAddVec
   (new_layer : AIG.RefVec aig (iter_num * w))
   (hold' : 2 * (iter_num - 1) < old_length)
   (old_layer_bv : BitVec (old_length * w))
-  (hval : 0 < l_length)
+  (_hval : 0 < l_length)
   (hw : 0 < w)
   -- the bits added already denote to the corresponding entry in acc
   (hold : ∀ (idx : Nat) (hidx : idx < old_length * w),