Nuprl Basics - Proof: sfa doc sexpr cases wf 1

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

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

T)+A)

Type
3. s : rec(T.(T

T)+A)
4. f : s1,s2:rec(T.(T

T)+A)

C(inl(<s1,s2>))
5. g : x:A

C(inr(x))

InjCase(s; s1s2. s1s2/s1,s2. f(s1,s2); x. g(x))

C(s)

By:	Analyze-3 THEN Analyze-1 THENL [Analyze-1;Id] THEN Reduce Concl

Generated subgoals:

1 6. x1 : rec(T.(TT)+A)
7. x2 : rec(T.(TT)+A)
f(x1,x2) C(inl(<x1,x2>))
Auto

2 6. y : A
g(y) C(inr(y))
Auto

About:

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

1	6. x1 : rec(T.(TT)+A) 7. x2 : rec(T.(TT)+A) f(x1,x2) C(inl(<x1,x2>))	Auto
2	6. y : A g(y) C(inr(y))	Auto