Skip to content
Snippets Groups Projects
Commit a1f630a6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Weaken monPred_bi_embedding. A bi index is always inhabited.

parent 128c9125
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 4 deletions
theories/bi/monpred.v
+ 2
− 4
View file @ a1f630a6
......@@ -468,8 +468,7 @@ Proof.
by apply affine, bi.forall_affine.
Qed.
Global Instance monPred_bi_embedding :
Inhabited I → BiEmbedding PROP (monPredI I PROP).
Global Instance monPred_bi_embedding : BiEmbedding PROP (monPredI I PROP).
Proof.
split; try apply _; unseal; try done.
- move =>?? /= [/(_ inhabitant) ?] //.
......@@ -501,7 +500,6 @@ Proof.
by apply timeless, bi.forall_timeless.
Qed.
Global Instance monPred_sbi_embedding :
Inhabited I → SbiEmbedding PROP (monPredSI I PROP).
Global Instance monPred_sbi_embedding : SbiEmbedding PROP (monPredSI I PROP).
Proof. split; try apply _. by unseal. Qed.
End sbi_facts.
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