proposition: Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y : (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
proof: Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)