Nuprl - Proof: hprod ty def 1

(10steps total) PrintForm Definitions hol pair Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hprod ty def 1

1. 'a : S
2. 'b : S

rep:(hprod('a; 'b)

hbool).

type_definition('a

hbool;hprod('a; 'b);is_pair;rep)

By:	((DTerm rep_prod 0) THEN (Unab [`type_definition`])) THEN Simp THEN StrongAuto

Generated subgoals:

1 3. x' : hprod('a; 'b)
4. x'' : hprod('a; 'b)
5. rep_prod(x') = rep_prod(x'')  'a'bhbool
  x' = x''
3 steps

2 3. x : 'a'bhbool
4. is_pair(x)
  x':hprod('a; 'b). x = rep_prod(x')  'a'bhbool
3 steps

3 3. x : 'a'bhbool
4. x':hprod('a; 'b). x = rep_prod(x')  'a'bhbool
  is_pair(x)
2 steps

About:

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

(10steps total) PrintForm Definitions hol pair Sections HOLlib Doc

1	3. x' : hprod('a; 'b) 4. x'' : hprod('a; 'b) 5. rep_prod(x') = rep_prod(x'') 'a'bhbool x' = x''	3 steps
2	3. x : 'a'bhbool 4. is_pair(x) x':hprod('a; 'b). x = rep_prod(x') 'a'bhbool	3 steps
3	3. x : 'a'bhbool 4. x':hprod('a; 'b). x = rep_prod(x') 'a'bhbool is_pair(x)	2 steps