1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
1 goal
I : biIndex
PROP : bi
P, Q : monPred
i : I
============================
"HW" : (P -∗ Q) i
--------------------------------------∗
(P -∗ Q) i
1 goal
I : biIndex
PROP : bi
P, Q : monPred
i, j : I
============================
"HW" : (P -∗ Q) j
"HP" : P j
--------------------------------------∗
Q j
1 goal
I : biIndex
PROP : bi
P, Q : monPred
Objective0 : Objective Q
𝓟, 𝓠 : PROP
============================
"H2" : ∀ i, Q i
"H3" : 𝓟
"H4" : 𝓠
--------------------------------------∗
∀ i, 𝓟 ∗ 𝓠 ∗ Q i
1 goal
I : biIndex
PROP : bi
FU : BiFUpd PROP
P, Q : monPred
i : I
============================
--------------------------------------∗
(Q -∗ emp) i
1 goal
I : biIndex
PROP : bi
FU : BiFUpd PROP
P : monPred
i : I
============================
--------------------------------------∗
∀ _ : (), ∃ _ : (), emp
The command has indeed failed with message:
Tactic failure: iFrame: cannot frame (P i).
1 goal
I : biIndex
hlc : has_lc
Σ : gFunctors
invGS_gen0 : invGS_gen hlc Σ
N : namespace
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟 ⎤
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
1 goal
I : biIndex
hlc : has_lc
Σ : gFunctors
invGS_gen0 : invGS_gen hlc Σ
N : namespace
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟 ⎤
--------------------------------------□
"Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
|
