Nuprl Basics - Proof: sfa doc sexpr atom wf 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sexpr atom wf 1 1 1 1

1. A : Type
2. s : rec(T.(T

T)+A)
3. Size(s) = 1
4. x1 : Sexpr(A)
5. x2 : Sexpr(A)
6. s = inl(<x1,x2>)
7. Size(s) = 1

s = Cons(x1;x2)

By:	Analyze THEN Def

Generated subgoals:

None

About:

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