IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr atom wf1112 1. A : Type
2. s : rec(T.(TT)+A)
3. Size(s) = 1
4. x1 : Sexpr(A)
5. x2 : Sexpr(A)
6. s = inl(<x1,x2>)
7. Size(Cons(x1;x2)) = 1
False
By:
Compute-1 Size(Cons(x1;x2)) * Size(x1)+Size(x2)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T)+A)
False
Size(Cons(x1;x2))
*
Size(x1)+Size(x2)
