Commit 39569586 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Prove map_Forall_delete.

parent c1c25def
......@@ -1119,6 +1119,8 @@ Proof.
naive_solver eauto using map_Forall_insert_11,
map_Forall_insert_12, map_Forall_insert_2.
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_ind (Q : M A Prop) :
( m i x, m !! i = None P i x map_Forall P m Q m Q (<[i:=x]>m))
Supports Markdown
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