Hi, is there a way to use the ssreflect `elim`

tactic with a custom induction principle, like `induction k using my_ind`

?

`elim/my_ind: t`

See https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#interpreting-eliminations for details

Thank you both! I wasn't looking in the right spot

Last updated: Jun 23 2024 at 03:02 UTC