From 5be9e48905514ae48f94d16fa119e3d2f2d96c56 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Sat, 11 Dec 2021 16:08:58 +0100
Subject: [PATCH] use proper names
---
iris_heap_lang/metatheory.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris_heap_lang/metatheory.v b/iris_heap_lang/metatheory.v
index 06738d24b..8f9718453 100644
--- a/iris_heap_lang/metatheory.v
+++ b/iris_heap_lang/metatheory.v
@@ -247,7 +247,7 @@ Proof.
x ∈ x2 :b: x1 :b: X →
binder_delete x1 (binder_delete x2 vs) !! x = None).
{ intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
- induction e=> X vs /= ? HX.
+ induction e as [| |f x e IHe | | | | | | | | | | | | | | | | | | | |]=> X vs /= ? HX.
3:{ f_equal. eapply IHe; eauto.
intros x0 Hx0.
rewrite !lookup_binder_delete_None.
--
GitLab