diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v index 0c363af6fa51bba5aa7894b2242545df454b3998..daba741fbf57cd027941fbb3924e1bea862dc2c8 100644 --- a/theories/bi/monpred.v +++ b/theories/bi/monpred.v @@ -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.