Ryan Shao (Mar 15 2023 at 19:27): Ryan Shao (Mar 15 2023 at 19:27):Hello,
I have a multiple-argument definition fun that takes in three arguments: l, f, and x. I'm proving it's equivalent to some result by inducting on l. As part of the inductive step, I invoke (fun l f (x + 1)), which I thought should be fine as I'm inducting on l and not x but this doesn't seem to work. Could I get some advice?
Mathias Fleury (Mar 15 2023 at 19:30):Usually you should use fun.induct instead of the induction principle from l
Mathias Fleury (Mar 15 2023 at 19:31):The other solution is induction l arbitrary: x
Last updated: Apr 19 2024 at 16:20 UTC