proposition: Lemma map_Exists_insert m i x : m !! i = None → map_Exists P (<[i:=x]>m) ↔ P i x ∨ map_Exists P m.
proof: Proof. naive_solver eauto using map_Exists_insert_1, map_Exists_insert_2_1, map_Exists_insert_2_2. Qed.
imports: Coq(Permutation) stdpp(options)