diff --git a/vest/Cargo.toml b/vest/Cargo.toml
index d92f236..9f04fa3 100644
--- a/vest/Cargo.toml
+++ b/vest/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "vest_lib"
-version = "0.0.1"
+version = "0.0.2"
 edition = "2021"
 license = "MIT"
 description = "VestLib: A library of formally verified parser and serializer combinators"
@@ -18,8 +18,6 @@ std = []
 
 [dependencies]
 vstd = "=0.0.0-2026-01-11-0057"
-#verus_builtin = "0.0.0-2025-08-12-1837"
-#verus_builtin_macros = "0.0.0-2025-12-07-0054"
 
 #vstd = { git = "https://github.com/verus-lang/verus", branch = "main" }
 #verus_builtin = { git = "https://github.com/verus-lang/verus", branch = "main" }
diff --git a/vest/src/regular/variant.rs b/vest/src/regular/variant.rs
index 94d82f7..cb52a8f 100644
--- a/vest/src/regular/variant.rs
+++ b/vest/src/regular/variant.rs
@@ -508,6 +508,7 @@ impl<Fst, Snd> SecureSpecCombinator for OptThen<Fst, Snd> where
     }
 
     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
+        vstd::slice::axiom_slice_ext_equal(&[true], &[true]);
         if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
             self.0.0.0.lemma_prefix_secure(s1, s2);
             self.0.0.lemma_parse_length(s1);