Is there a one-tactic way of replacing "h: (a1,b1)=(a2,b2)" (for a given product type A*B) by "ha: a1=a2" and "hb: b1=b2" in the context? destruct does not work. I have a way to do this in several steps but it doesn't look optimal...
injection h. Or injection h as as [= [ha hb]]?
or ssreflect's "move: h => [ha hb]", which is basically the same syntax as for ssreflect's destruct
@Paolo Giarrusso Got it. Thank you very much!
Last updated: Dec 05 2023 at 05:01 UTC