Nuprl - Proof: hsum iso def 1 2 2 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum iso def 1 2 2 1 1 2

1. 'a : S
2. 'b : S
3. y : 'b
4. x : 'a
5. (

u:'a+'b. InjCase(u
5. (

u:'a+'b. InjCase; p.

x:'a.

y:'b. (x =

b
5. (

u:'a+'b. InjCase; q.

x:'a.

y:'b. (y =

b))
5. (inr(y))
5. =
5. (

u:'a+'b. InjCase(u
5. (

u:'a+'b. InjCase; p.

x:'a.

y:'b. (x =

b
5. (

u:'a+'b. InjCase; q.

x:'a.

y:'b. (y =

b))
5. (inl(x))

inr(y) = inl(x)

'a+'b

By:	((EquandMap (f.f(true,x,arb('b))) 5) THEN (Thin 5)) THEN Try (Complete Auto) THEN Simp

Generated subgoal:

1 5. True
inr(y) = inl(x) 'a+'b
1 step

About:

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