Is there a nice way to match! on projections in Ltac2 such that the branch also matches the primitive, unfolded form of the projection?
match!
Last updated: Jan 29 2023 at 05:03 UTC