proofmode_monpred.ref

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,⊤}=> ⎡ ▷ 𝓟 ⎤