Commit 68d1ee20 authored by Ralf Jung's avatar Ralf Jung

need to replace some more firstorder

parent 82d3fc4f
Pipeline #25491 passed with stage
in 30 minutes and 24 seconds
......@@ -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').
......
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