Commit 48be18be authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove unused parameters from some boxes lemmas.

parent 3663aaf3
...@@ -160,7 +160,7 @@ Proof. ...@@ -160,7 +160,7 @@ Proof.
iFrame; eauto. iFrame; eauto.
Qed. Qed.
Lemma box_fill_all f P Q : box N f P P ={N}= box N (const true <$> f) P. Lemma box_fill_all f P : box N f P P ={N}= box N (const true <$> f) P.
Proof. Proof.
iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_sepM_fmap. iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
...@@ -175,7 +175,7 @@ Proof. ...@@ -175,7 +175,7 @@ Proof.
iApply "Hclose". iNext; iExists true. by iFrame. iApply "Hclose". iNext; iExists true. by iFrame.
Qed. Qed.
Lemma box_empty_all f P Q : Lemma box_empty_all f P :
map_Forall (λ _, (true =)) f map_Forall (λ _, (true =)) f
box N f P ={N}= P box N (const false <$> f) P. box N f P ={N}= P box N (const false <$> f) P.
Proof. Proof.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment