From fafe68cc4512e3dd4b73388f6de5045cfc1f1969 Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 7 Apr 2022 18:07:35 +0900
Subject: [PATCH] Minor fix
---
theories/typing/lib/cell.v | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index fa0d42a1..7893d0eb 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -286,13 +286,12 @@ Section cell.
case x as [[|x|]|]=>//=. rewrite split_mt_uniq_bor.
iDestruct "box" as "[[#In ↦uniq] †]". wp_bind Skip.
iApply (wp_cumulative_time_receipt with "TIME"); [done|]. wp_seq.
- iIntros "⧗". wp_seq. iDestruct "↦uniq" as (?? ξi [? Eq]) "(↦ & Vo & Bor)".
+ iIntros "⧗". iDestruct "↦uniq" as (?? ξi [? Eq]) "(↦ & Vo & Bor)".
move: Eq. set ξ := PrVar _ ξi=> Eq.
iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
iMod (bor_acc_cons with "LFT Bor α") as
- "[(%&%&_& Pc &%& >↦' & %Φ & big) ToBor]"; [done|].
- iMod (bi.later_exist_except_0 with "big") as (aπ ?) "(>->& >Obs' & >#⧖ & ty)".
- iCombine "Obs Obs'" as "Obs".
+ "[(%&%&_& Pc &%& >↦' & %Φ & big) ToBor]"; [done|]. wp_seq.
+ iDestruct "big" as (aπ ?->) "(Obs' & #⧖ & ty)". iCombine "Obs Obs'" as "Obs".
iMod (cumulative_persistent_time_receipt with "TIME ⧗ ⧖") as "#⧖S"; [done|].
iMod (uniq_strip_later with "Vo Pc") as (Eq' <-) "[Vo Pc]".
have ->: vπ = λ π, (Φ, π ξ). { by rewrite [vπ]surjective_pairing_fun Eq Eq'. }
--
GitLab