(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
  'a,'b:S.
  equal
  (rep_prod
  ,select
  ,(rep:hprod('a; 'b)
  ,( 'a
  ,( 'b
  ,( hbool. and
  ,( hbool. (all
  ,( hbool. ((p':hprod('a; 'b). all
  ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). implies
  ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (equal
  ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ((rep(p')
  ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (,rep(p''))
  ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ,equal(p',p''))))
  ,( hbool. ,all
  ,( hbool. ,(p:'a  'b  hbool. equal
  ,( hbool. ,(p:'a  'b  hbool. (is_pair(p)
  ,( hbool. ,(p:'a  'b  hbool. ,exists
  ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). equal
  ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). (p
  ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). ,rep(p'))))))))
By: HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))
THEN
Try
(Complete
((Unfold `label` 0 THEN MemEqCD THEN Try (Complete Auto) THEN Unfold `label` 0
((THEN
((MemEqCD
((THEN
((Try (Complete Auto)
((THEN
((Unfold `label` 0
((THEN
((Try (Complete Auto)))

Generated subgoal:

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'))))))))
2 steps

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

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