Nuprl Basics - Proof: sfa doc sexpr case thm 1 1 1

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

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

T)+A)
3. v1 : Sexpr(A)
4. v2 : Sexpr(A)
5. s = inl(<v1,v2>)

(

x:A. Cons(v1;v2) = Inj(x))

(

s1,s2:Sexpr(A). Cons(v1;v2) = Cons(s1;s2))

By:

Select: 2

Generated subgoal:

1 s1,s2:Sexpr(A). Cons(v1;v2) = Cons(s1;s2)
1 step

About:

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