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?
Usually you should use
fun.induct instead of the induction principle from l
The other solution is
induction l arbitrary: x
Last updated: Dec 07 2023 at 20:16 UTC