From 626784fdca24b100ed4ba682132ce9cd9bff338b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Feb 2021 13:16:35 +0100
Subject: [PATCH] Tweak shady proof.
---
theories/examples/subprotocols.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 8f848a6..57030fd 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 :
--
GitLab