(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 1 1

1. 'a : S
2. 'b : S
3. x' : hprod('a'b)
4. x'' : hprod('a'b)
5. (a:'ab:'b. (a = 1of(x'))(b = 2of(x')))
5. =
5. (a:'ab:'b. (a = 1of(x''))(b = 2of(x'')))
6. 1of(x') = 1of(x'')
7. 2of(x') = 2of(x'')
  x' = x''


By: Analyze 4 THEN Analyze 3 THEN Simp THEN StrongAuto THEN Analyze THEN StrongAuto


Generated subgoals:

None

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

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