Guillaume Dubach (Oct 31 2020 at 09:10): Guillaume Dubach (Oct 31 2020 at 09:10):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...
Paolo Giarrusso (Oct 31 2020 at 10:01):injection h. Or injection h as as [= [ha hb]]?
Paolo Giarrusso (Oct 31 2020 at 10:02):or ssreflect's "move: h => [ha hb]", which is basically the same syntax as for ssreflect's destruct
Guillaume Dubach (Oct 31 2020 at 16:54):@Paolo Giarrusso Got it. Thank you very much!
Last updated: Dec 05 2023 at 05:01 UTC