From 176c5169630f357e2aa1c2155ec15162c5c5657c Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 14 Sep 2020 18:43:29 +0200
Subject: [PATCH] Proof nits
---
theories/logrel/session_types.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index f319581..33246eb 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.
--
GitLab