(3steps total) PrintForm Definitions Lemmas hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hrep prod wd 1
1. 'a : S
2. 'b : S
  rep_prod
  =
  (@rep:hprod('a; 'b)  'a  'b  hbool
  (@((p',p'':hprod('a; 'b).  ((rep(p')) = (rep(p'')))(p' = p''))
  (@(x:'a  'b  hbool
  (@(((is_pair(x)) = (p':hprod('a; 'b). (x = (rep(p'))))))))
By: Unab [`hrep_prod`;`hmk_pair`] THEN AbReduce 0

Generated subgoal:

1   (p:'a'b. a:'a. b:'b. (a = 1of(p))(b = 2of(p)))
  =
  (@rep:hprod('a; 'b)  'a  'b  hbool
  (@((p',p'':hprod('a; 'b).  ((rep(p')) = (rep(p'')))(p' = p''))
  (@(x:'a  'b  hbool
  (@(((is_pair(x)) = (p':hprod('a; 'b). (x = (rep(p'))))))))
1 step

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

(3steps total) PrintForm Definitions Lemmas hol pair Sections HOLlib Doc