Commit 787636f5 authored by Robbert Krebbers's avatar Robbert Krebbers

Avoid use of `firstorder`.

parent faace489
Pipeline #15958 passed with stage
in 16 minutes
......@@ -934,8 +934,8 @@ Section map2.
- apply and_elim_r.
- rewrite <- (left_id True%I ()%I (Φ i x1 x2)).
apply and_mono=>//. apply pure_mono=>_ k.
rewrite !lookup_insert_is_Some' !lookup_empty.
firstorder.
rewrite !lookup_insert_is_Some' !lookup_empty -!not_eq_None_Some.
naive_solver.
Qed.
Lemma big_sepM2_fmap {A' B'} (f : A A') (g : B B') (Φ : nat A' B' PROP) m1 m2 :
......
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