diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 8f848a6a3350cd72bbc674a56c855f88656df2e7..57030fd0cdd5cf248a0d71a9d899adb83c651b9d 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -66,10 +66,10 @@ Section subprotocol_basics.
   Proof.
     iIntros "H".
     iInduction (xs) as [|x xs] "IH" forall (v).
-    - eauto.
-    - iDestruct "H" as (v' Heq) "H".
-      iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
-      iExists (#x::ws)=> /=; eauto.
+    { iExists []; eauto. }
+    iDestruct "H" as (v' ->) "H".
+    iDestruct ("IH" with "H") as (ws) "[Hlist Heq]".
+    iExists (#x :: ws); simpl; eauto.
   Qed.
 
   Lemma list_length_example :