Hello! I'm running with Mangle Names in order to ensure that my proofs aren't dependent on generated names. For some reason, I'm stuck trying to supply a name for a generated induction hypothesis. There doesn't seem to be a way to tell the induction tactic what name to use... Is this expected right now?
Do you mean that
induction ... as doesn't work?
Sorry, I've just realized I made a mistake. I was missing the last parameter to
as, so the induction hypothesis was using a generated name.
Last updated: Jan 27 2023 at 01:03 UTC