diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index f3195816888de52541d83a17e7c01fd04b717eb6..33246ebb45fc17a4b0a8ae5ad6867a7a07b48ddb 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -112,10 +112,10 @@ Section session_types.
            (@lty_choice Σ a).
   Proof.
     intros n Ss Ts Heq. rewrite /lty_choice.
-    do 4 f_equiv.
+    do 2 f_equiv. f_equiv => i.
     rewrite !lookup_total_alt.
-    specialize (Heq a0).
-    destruct (Ss !! a0), (Ts !! a0);
+    specialize (Heq i).
+    destruct (Ss !! i), (Ts !! i);
       [ f_contractive | contradiction | contradiction | done ].
     - f_equiv. split; intros H; eauto.
     - by rewrite Heq.