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