induction with, with implicit arguments

Stream: Is there code for X?

[Antoine Chambert-Loir]

What is the syntax for induction when the inductive assertions have implicit arguments, such as docs#Finset.induction_on ?
I wanted to type

induction s using Finset.induction_on with
| empty => ...
| insert {a} {s} has ih => …

but that doesn't seem to work.

[Eric Wieser]

| @insert a s has ih => …, I think