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:
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_indterms are noncanonical. These noncanonical terms are redices with principal argument r and contracta
when r is canonical. The rules for binding variables are:
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.