Commit a6f30595 authored by Ralf Jung's avatar Ralf Jung

add map_Forall_lookup

parent 432120a3
......@@ -1234,6 +1234,9 @@ Proof.
Qed.
Lemma map_Forall_delete m i : map_Forall P m map_Forall P (delete i m).
Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
Lemma map_Forall_lookup m i x :
m !! i = Some x map_Forall P m P i x.
Proof. intros Hlk Hm. by apply Hm. Qed.
Lemma map_Forall_foldr_delete m is :
map_Forall P m map_Forall P (foldr delete m is).
Proof. induction is; eauto using map_Forall_delete. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment