Cannot iApply lemma with let-binder and bi_emp_valid
The following script fails:
Lemma test_iPoseProof_let2 P Q :
(let R := True%I in ⊢ R ∗ P -∗ Q) →
P ⊢ Q.
Proof.
iIntros (help) "HP".
iPoseProof (help with "[$HP]") as "?". done.
Qed.
It says (notation printing due to this being in !791 (merged))
Error: Tactic failure: iPoseProof: (let R := True%I in R ∗ P -∗ Q) not a BI assertion.
If I move the ⊢ between R ∗ P
and Q
, it works, so this is related to bi_entails vs bi_emp_valid somehow.