NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Cons(s1;s2) == inl(<s1,s2>)

is mentioned by

Thm* a,b,c:X.
Thm* Reverse(Cons(Inj(a);Cons(Inj(b);Inj(c))))
Thm* =
Thm* Cons(Cons(Inj(c);Inj(b));Inj(a))
[sfa_doc_sexpr_reverse_example]
Thm* Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) = 3  [sfa_doc_sexpr_size_example]
Thm* A:Type, C:(Sexpr(A)Type), s:Sexpr(A),
Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))).
Thm* (Case of s :  Inj(x g(x) ; Cons(s1;s2 f(s1,s2))  C(s)
[sfa_doc_sexpr_cases_wf]
Thm* s:Sexpr(A). (x:As = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))[sfa_doc_sexpr_case_thm]
Def Reverse(e)
Def == Case of e
Def == CaInj(x Inj(x)
Def == CaCons(s1;s2 Cons(Reverse(s2);Reverse(s1))
Def (recursive)
[sfa_doc_sexpr_reverse]

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

NuprlPrimitives Sections NuprlLIB Doc