proposition: Lemma map_lookup_compose_Some m n a c : (m ∘ₘ n) !! a = Some c ↔ ∃ b, n !! a = Some b ∧ m !! b = Some c.
proof: Proof. rewrite map_lookup_compose. destruct (n !! a) eqn:?; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)