proposition: Lemma map_Forall_insert m i x : m !! i = None → map_Forall P (<[i:=x]>m) ↔ P i x ∧ map_Forall P m.
proof: Proof. naive_solver eauto using map_Forall_insert_1_1, map_Forall_insert_1_2, map_Forall_insert_2. Qed.
imports: Coq(Permutation) stdpp(options)