Rule keyword can be ommitedSynopsis:

`rule tacletname on=<TERM> formula=<TERM> occ=<INT>`

**Arguments:**

- rulename :
*STRING*name of taclet to apply `on`

:*TERM*(find term of the taclet)`formula`

:*TERM*(top-level formula in which term appears)`occ`

:*INT*(occurrence number of term formula in sequent)