The proof rules will ensure that the following two assertions hold.

That is,rec(x,y.A;b)type

&x:(B->Uk)->y:B->Atype

rec(x,y.A;b)rec(x,y.A;b)type

&`\`

y.rec(x,y.A;y)

Thu Sep 14 08:45:18 EDT 1995