Nuprl Basics - Proof: sfa doc sexpr atom wf 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. 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>)

False

By:	Hyp:3 Asserted THEN Subst-1: s = Cons(x1;x2) Sexpr(A)

Generated subgoals:

1 7. Size(s) = 1
s = Cons(x1;x2)
1 step

2 7. Size(Cons(x1;x2)) = 1
False
1 step

About:

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

1	7. Size(s) = 1 s = Cons(x1;x2)	1 step
2	7. Size(Cons(x1;x2)) = 1 False	1 step