INDUCTIVE DEFINITION T () [ ]
OF ARITY
Set
BUILT FROM:
TSort:
nat
→
T
| TLRef:
nat
→
T
| THead:
K
→
T
→
T
→
T