Commit 03127e9d authored by Robbert Krebbers's avatar Robbert Krebbers

Fix weird thing that should not have worked.

parent 862c6904
Pipeline #15531 passed with stage
in 8 minutes and 24 seconds
......@@ -215,7 +215,7 @@ Proof.
by rewrite multiplicity_disj_union, multiplicity_empty.
Qed.
Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ().
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
Proof. intros X. by rewrite (comm_L ()), (left_id_L _ _). Qed.
Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ).
Proof.
......
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