1. n : 
2. f : n
3. g : n
4. x:. g(f(x)) = x
5. y:n. f(g(y)) = y
   ~ (n+1)

By:	(Witness: x.if x=0 n else f(x-1) fi with type (n+1) (THEN (Witness: y.if y=n 0 else g(y)+1 fi with type (n+1)) THENA (Analyze THEN (SplitITE Concl))

1

6. (x.if x=0 n else f(x-1) fi)  (n+1) 7. (y.if y=n 0 else g(y)+1 fi)  (n+1)   InvFuns(;(n+1);x.if x=0 n else f(x-1) fi;y.if y=n 0 else g(y)+1 fi)

3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html