elimType

elimType T using th hyps

Synopsis:

elimType sterm [using sterm] intros-spec

Pre-conditions:

T must be an inductive type.

Action:

TODO (severely bugged now).

New sequents to prove:

TODO