a META and not an application.
* The old implementation of ElimIntros was misleading: It applied Intros only
to the first goal. Removed.
* A new implementation of ElimIntros (and of ApplyIntros) is partially provided,
but unused. It requires the forthcoming new META definition and unification
algorithm.