(7steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sexpr atom wf 1 1
1. A : Type
2. s : rec(T.(TT)+A)
3. Size(s) = 1
4. s1 : (Sexpr(A)Sexpr(A))+A
5. s = s1
  sexprAtom(s1)  A
By: Analyze-2 THENL [Analyze-2 THEN False  Asserted;Id]

Generated subgoals:

1 4. x1 : Sexpr(A)
5. x2 : Sexpr(A)
6. s = inl(<x1,x2>)  (Sexpr(A)Sexpr(A))+A
  False
3 steps
2 4. y : A
5. s = inr(y)  (Sexpr(A)Sexpr(A))+A
  sexprAtom(inr(y))  A
1 step

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

(7steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc