diff --git a/theories/base_logic/block_ends.v b/theories/base_logic/block_ends.v
index 4901aa70700b3848070bb8f51004c820f951de81..08da118bca27792017a455d4903a387864fb85d5 100644
--- a/theories/base_logic/block_ends.v
+++ b/theories/base_logic/block_ends.v
@@ -74,7 +74,7 @@ Section Mblock_ends.
destruct (mblock_ends m !! i) as [a|] eqn:Ha.
- move : Ha. rewrite !map_filter_lookup_Some.
move => [Hi FA].
- have ?: k ≠ i by firstorder.
+ have ?: k ≠ i by naive_solver.
split; [by rewrite lookup_insert_ne|].
move => k' v' Hk'.
case (decide (k' = k)) => ?.
@@ -89,7 +89,7 @@ Section Mblock_ends.
+ inversion Hv'. subst v'.
destruct sR as [k' [v' [Hk' HR]]].
move => /(_ k' v') HE.
- have ?: k ≠ k' by firstorder.
+ have ?: k ≠ k' by naive_solver.
apply HE; [|done|done]. by rewrite lookup_insert_ne.
+ destruct Hi as [Hi|FAi]; [by rewrite Hi in Hv'|].
move => FA. apply (FAi _ Hv').