Commit 06f3218d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Weaken premise of `gmultiset_local_update_dealloc`.

parent b91b45a1
......@@ -73,9 +73,10 @@ Section gmultiset.
Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
Lemma gmultiset_local_update_dealloc X Y X' :
X' X X' Y (X,Y) ~l~> (X X', Y X').
X' Y (X,Y) ~l~> (X X', Y X').
intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
apply gmultiset_local_update. apply gmultiset_eq=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
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