diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v index fa0d42a10123dbd92f6bcc59f9215a4510bcffe0..7893d0eb987de3c29d1b20a79de93216be9c4242 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'. }