elimType T using th hyps
elimType sterm [using sterm] intros-spec
T must be an inductive type.
TODO (severely bugged now).
TODO