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

By:	New:v Analyze-2 THENL [Analyze-2;Id] THEN Def of Inj(<sexpr atom>) | Cons(<sexpr>;<sexpr>)

1	3. v1 : Sexpr(A) 4. v2 : Sexpr(A) 5. s = inl(<v1,v2>)  (Sexpr(A)Sexpr(A))+A   (x:A. Cons(v1;v2) = Inj(x))  (s1,s2:Sexpr(A). Cons(v1;v2) = Cons(s1;s2))	2 steps
2	3. y : A 4. s = inr(y)  (Sexpr(A)Sexpr(A))+A   (x:A. Inj(y) = Inj(x))  (s1,s2:Sexpr(A). Inj(y) = Cons(s1;s2))	2 steps

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