`leibnizO` finds convoluted proof for definitions
Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)Require Import iris.algebra.ofe.
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. rewrite /tagO /natO /tag. reflexivity.
(* Why doesn't this hold? *)