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: Oct 03 2023 at 02:34 UTC
Janno (Sep 04 2020 at 15:12): Janno (Sep 04 2020 at 15:12):