The dom predicate defined earlier in the chapter is used here to demonstrate induction. Given the definitions
~<T>== (<T>) -> void
some <v>:<A>.<P>== <v>:(<A>)#(<P>)
N== {n:int| ~(n<0)}
true== (0 in int)
D(<x>)== rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); <x>)
figure 
sketches the proof of
f:N->N, r:D(0) >> some y:N. f(y)=0.Although D(0) is inhabited only by axiom, evaluating the extracted term produces a root.
Figure: A Sample Proof Using Recursion