fixed name, indentation and generalized thm

leanprover · Oct 7, 2024 · 2059f29 · 2059f29
1 parent 5da12c5
commit 2059f29
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Proofs/SHA512/SHA512_block_armv8_rules.lean b/Proofs/SHA512/SHA512_block_armv8_rules.lean
@@ -138,8 +138,8 @@ theorem truncate_of_concat_is_lsb_64 (x y : BitVec 64) :
   BitVec.zeroExtend 64 (x ++ y) = y := by
   bv_check "lrat_files/Sha512_block_armv8_rules.lean-truncate_of_concat_is_lsb_64-106-2.lrat"
 
-theorem zeroExtend_append_eq (w : Nat) (x y : BitVec w) :
-  BitVec.zeroExtend w (x ++ y) = y := by
+theorem zeroExtend_append_eq_right {w v : Nat} {x : BitVec w} {y : BitVec v} :
+    BitVec.zeroExtend v (x ++ y) = y := by
   ext
   simp only [truncate_append, Nat.le_refl, ↓reduceDIte, zeroExtend_eq]