Nuprl - Proof: hsum iso def 1 2 2

(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. 'a : S
2. 'b : S

type_definition(

'a

'b

;'a+'b;

f:

'a

'b

.

u:'a+'b

type_definition(

'a

'b

;'a+'b;

f:

'a

'b

.

(f

type_definition(

'a

'b

;'a+'b;

f:

'a

'b

.

=

(rep_sum

type_definition(

'a

'b

;'a+'b;

f:

'a

'b

.

=

((u)));rep_sum)

By:	Unab [`type_definition`] THEN Try (Complete Auto)

Generated subgoal:

1   (x',x'':'a+'b. rep_sum(x') = rep_sum(x'')  'a'b  x' = x'')
  & (x:('a'b).
  & ((f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)
  & (
  & ((x':'a+'b. x = rep_sum(x')  'a'b))
11 steps

About:

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

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