`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? *)