Matita Home
elimType sterm [using sterm] [<intros_spec>]
Prev
Chapter 6. Tactics
Next
elimType
sterm
[using
sterm
] [<intros_spec>]
elimType T using th hyps
Pre-conditions:
T
must be an inductive type.
Action:
TODO (severely bugged now).
New sequents to prove:
TODO