proposition: Lemma map_imap_ext {A1 A2 B} (f1 : K → A1 → option B) (f2 : K → A2 → option B) (m1 : M A1) (m2 : M A2) : (∀ k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k)) → map_imap f1 m1 = map_imap f2 m2.
proof: Proof. intros HExt. apply map_eq. intros i. rewrite !map_lookup_imap. specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)