(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum iso def 1 2 2 1 1
1. 'a : S
2. 'b : S
  x',x'':'a+'b. rep_sum(x') = rep_sum(x'')  'a'b  x' = x''
By: Auto THEN Analyze 4 THEN Analyze 3 THEN Unab [`hrep_sum`]

Generated subgoals:

1 3. x1 : 'a
4. x : 'a
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. (inl(x1))
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. (inl(x))
  inl(x1) = inl(x)  'a+'b
2 steps
2 3. y : 'b
4. x : 'a
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))
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. (inl(x))
  inr(y) = inl(x)  'a+'b
2 steps
3 3. x : 'a
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. (inl(x))
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))
  inl(x) = inr(y)  'a+'b
2 steps
4 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
2 steps

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

(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc