proposition: Lemma map_Forall_insert_1_2 m i x : m !! i = None → map_Forall P (<[i:=x]>m) → map_Forall P m.
proof: Proof. intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence. Qed.
imports: Coq(Permutation) stdpp(options)