Add terms
rec(z,x.T;a)where u,v,x and z range over variables, a,g,r and T range over terms, and T is restricted as follows:
rec_ind(r; v,u.g)
No instance of z bound by rec may 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.Thus (A#z)->B or f(inr z) or spread(z; a,b.a->int)\ cannot be subexpressions of T. When closed, rec terms are canonical and
rec_ind terms are noncanonical. These noncanonical terms
are redices with principal argument r and
contracta
when r is canonical. The rules for binding variables are:\u.rec_ind(u; v,u.g),
rec_ind( r; v,u.g)
the u and v in front of the dot and
any free occurrences of u or v in g become bound.