Assuming there are `n`

goals, `map_tacs [t1; t2; ...; tn]`

applies each `ti`

to the respective
goal and leaves the resulting subgoals.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`t <;> [t1; t2; ...; tn]`

focuses on the first goal and applies `t`

, which should result in `n`

subgoals. It then applies each `ti`

to the corresponding goal and collects the resulting
subgoals.

## Equations

- One or more equations did not get rendered due to their size.