proposition: Lemma map_ind {A} (P : M A → Prop) : P ∅ → (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) → ∀ m, P m.
proof: Proof. intros ? Hins m. induction (map_wf m) as [m _ IH]. destruct (map_choose_or_empty m) as [(i&x&?)| ->]; [|done]. rewrite <-(insert_delete m i x) by done. apply Hins; [by rewrite lookup_delete|]. by apply IH, delete_subset. Qed.
imports: Coq(Permutation) stdpp(options)