Add terms

whererec(z,x.T;a)

`rec_ind(`

r;v,u.g)

No instance ofThuszbound byrecmay occur in the domain type of a function space, in the argument of a function application or in the principal argument(s) of the remaining elimination forms.

`rec_ind`

terms are noncanonical. These noncanonical terms
are redices with principal argument when`\`

u`.rec_ind(`

,u;v,u.g)

- In
`rec(`the**z**,**x**.**T**;**a**)**z**and**x**in front of the dot and any free occurrences of**z**or**x**in**T**become bound. - In
`rec_ind(`

**r**;**v**,**u**.**g**)**u**and**v**in front of the dot and any free occurrences of**u**or**v**in**g**become bound.

Thu Sep 14 08:45:18 EDT 1995