Li-yao (Jan 07 2021 at 21:34): Li-yao (Jan 07 2021 at 21:34):existT _ x f = existT _ y g is something you can actually invert if y and g are variables. Is there a tactic for doing that? I'm actually looking for a way that would work for any inductive type, but I'm not sure how to turn a constructor into a pattern.
One other step that seems useful for that is to generalize all hypotheses depending on y and g, but generalize dependent y mixes g and the aforementioned equality with everything else. Is there a tactic that would generalize everything that depends on multiple given variables, and either keeps those variables in the context or at least at the head of the goal?
Paolo Giarrusso (Jan 07 2021 at 22:45):Was inversion_sigma related?
Paolo Giarrusso (Jan 07 2021 at 22:45):(To the first)
Li-yao (Jan 07 2021 at 22:49):Indeed that looks like it for sigma!
Last updated: Oct 01 2023 at 19:01 UTC