Skip to content
Snippets Groups Projects

Flip direction of `map_disjoint_fmap`.

Merged Robbert Krebbers requested to merge robbert/map_disjoint_fmap into master
1 file
+ 1
1
Compare changes
  • Side-by-side
  • Inline
+ 1
1
@@ -2054,7 +2054,7 @@ Proof.
Qed.
Lemma map_disjoint_fmap {A B} (f1 f2 : A B) (m1 m2 : M A) :
m1 ## m2 f1 <$> m1 ## f2 <$> m2.
f1 <$> m1 ## f2 <$> m2 m1 ## m2.
Proof.
rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
Qed.
Loading