decompose [as id…]

None.

For each each premise H of type T in the current context where T is a non-recursive inductive type without right parameters and of sort Prop or CProp, the tactic runs elim H as H₁ ... H_m , clears H and runs itself recursively on each new premise introduced by elim in the opened sequents.

The ones generated by all the elim tactics run.