We define 
, a syntactic transformation on terms, as follows.
f [t]
= 
t
#f '(t),
if f
had been bound by the the first variable in a surrounding fix term.
Recall that 
is the characteristic function for the domain of f.
t[a]
= 
t
#
a
#
dom(t)(a) if the first clause does not apply.
t(a)
= 
t
#
a
spread(e; u,v.t)
=
e
#
spread(e; u,v.
t
), and
similarly for the other elimination forms.
inl(a)
= 
a
<a,b>
= 
a
#
b
t
= true, for the remaining terms.