1. 'a : S
2. 'b : S
3. y1 : 'b
4. y : 'b
5. (u:'a+'b. InjCase(u
5. (u:'a+'b. InjCase; p. b:. x:'a. y:'b. (x = p)b
5. (u:'a+'b. InjCase; q. b:. x:'a. y:'b. (y = q)b))
5. (inr(y1))
5. =
5. (u:'a+'b. InjCase(u
5. (u:'a+'b. InjCase; p. b:. x:'a. y:'b. (x = p)b
5. (u:'a+'b. InjCase; q. b:. x:'a. y:'b. (y = q)b))
5. (inr(y))
  inr(y1) = inr(y)  'a+'b

By:	((EquandMap (f.f(false,arb('a),y1))  5) THEN (Thin 5) THEN Simp) THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1

5. y1 = y   inr(y1) = inr(y)  'a+'b

1 step

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