Fix some proofs

AeneasVerif · Nov 12, 2024 · 501ea67 · 501ea67
1 parent f15f8ed
commit 501ea67
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
@@ -943,10 +943,8 @@ theorem insert_spec {α} (hm : HashMap α) (key : Usize) (value : α)
   split
   . split
     . simp_all (config := {maxDischargeDepth := 1})
-      tauto
     . progress as ⟨ hm2 ⟩
       simp_all (config := {maxDischargeDepth := 1})
-      tauto
   . simp_all (config := {maxDischargeDepth := 1})
 
 @[pspec]