printing universes reveals the two arguments have different universes, while with the stdlib no universes appear. I don't know if that's supposed to count as "syntactically different", but that would be reasonable

```
t@{hott.67}
(underlying_natural@{hott.74 hott.75} (S n)
(s@{hott.76 hott.77 hott.78 hott.79 hott.74 hott.75} n i y1))
(underlying_natural@{hott.82 hott.83} (S n)
(s@{hott.76 hott.77 hott.78 hott.79 hott.82 hott.83} n i y1))
```

Meanwhile, this works, but has a very different meaning. `unify`

can perform lots of computation in general

```
match goal with
| [ H : lt ?n1 ?n2 |- _ ] => unify n1 n2; idtac n1 n2
end.
```

constr_eq should be enough

yep

nice thanks!

Patrick Nicodemus has marked this topic as resolved.

Last updated: Feb 06 2023 at 12:04 UTC