Commit 736b17dc authored by Robbert Krebbers's avatar Robbert Krebbers

Weaken premise of `gmultiset_local_update_dealloc`.

parent 8f41613d
......@@ -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').
Proof.
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).
lia.
......
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