proposition: Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j : alter f i m !! j = None ↔ m !! j = None.
proof: Proof. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne. Qed.
imports: Coq(Permutation) stdpp(options)