diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs
index 4e3529b..7dcac07 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs
@@ -971,6 +971,7 @@ impl<A> Seq<Seq<A>> {
             self.len() == 1 ==> self.flatten() == self.first(),
     {
         broadcast use Seq::add_empty_right;
+
         if self.len() == 1 {
             assert(self.flatten() =~= self.first().add(self.drop_first().flatten()));
         }
@@ -1022,6 +1023,7 @@ impl<A> Seq<Seq<A>> {
         decreases self.len(),
     {
         broadcast use Seq::add_empty_right, Seq::push_distributes_over_add;
+
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
             seq![self.last()].lemma_flatten_one_element();
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index f35037b..ff4095e 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -1990,6 +1990,7 @@ mod m4 {
                 p.inv(),
         {
             broadcast use Ring::properties;
+
             assert(p.spec_succ().spec_prev() == p);
             assert(p.spec_prev().spec_succ() == p);
         }