proposition: Lemma map_Forall_ind (Q : M A → Prop) : Q ∅ → (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) → ∀ m, map_Forall P m → Q m.
proof: Proof. intros Hnil Hinsert m. induction m using map_ind; auto. rewrite map_Forall_insert by done; intros [??]; eauto. Qed.
imports: Coq(Permutation) stdpp(options)