TYPESUBST is a top-level command.
Substitute for a type variable in one line to infer another line.
The type variable must not appear in any hypothesis.
The command format for TYPESUBST is:

 <n>TYPESUBST    D    P     A       B 

The arguments have the following meaning:
D : Line before Type Substitution
P : Line after Type Substitution
A : Type Variable
B : Type to Substitute for Type Variable

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage