diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs
index 8259af85f..87aad43ec 100644
--- a/src/v2/kubernetes_cluster/proof/network_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/network_liveness.rs
@@ -28,9 +28,10 @@ pub open spec fn no_req_before_rpc_id_is_in_flight(rpc_id: RPCId) -> StatePred<C
 // It's only related to the message.
 //
 // In detail, we have to show two things:
-//     a. Newly created api request message satisfies requirements: s.in_flight(msg) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime).
-//     b. The requirements, once satisfied, won't be violated as long as the message is still in flight:
-//         s.in_flight(msg) /\ requirements(msg, s) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime).
+//      a. Newly created api request message satisfies requirements:
+//          s.in_flight(msg) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime).
+//      b. The requirements, once satisfied, won't be violated as long as the message is still in flight:
+//          s.in_flight(msg) /\ requirements(msg, s) /\ s_prime.in_flight(msg) ==> requirements(msg, s_prime).
 //
 // Previously, when "requirements" was irrelevant to the state, b will be sure to hold. Later, we find that "requirements" in some
 // case does need some information in the state. So we add state as another parameter and requires the caller of the lemma