1. A : Type
2. s : Sexpr(A)
  (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))

1

2. s : rec(T.(TT)+A) 3. u : (Sexpr(A)Sexpr(A))+A 4. s = u  (Sexpr(A)Sexpr(A))+A   (x:A. u = Inj(x))  (s1,s2:Sexpr(A). u = Cons(s1;s2))

5 steps

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