From 79da67c948ecda836c8f1d2ea34eef2efdc46383 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dani=C3=ABl=20Louwrink?= <daniel.louwrink@gmail.com>
Date: Wed, 6 May 2020 14:48:06 +0200
Subject: [PATCH] fix pair example
---
theories/logrel/examples/pair.v | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 77074ab..427c357 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -11,6 +11,8 @@ Section pair.
Proof.
rewrite /prog.
iApply ltyped_lam. iApply ltyped_pair.
- iApply ltyped_recv. iApply ltyped_recv.
+ iApply ltyped_recv.
+ 2:{ iApply ltyped_recv. by rewrite /binder_insert lookup_insert. }
+ by rewrite lookup_insert.
Qed.
End pair.
--
GitLab