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