(8steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnil def 1

1. 'a : S
  nil = abs_list(<n:hnum. @e:'a. true,0>)


By: Inst
Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'ar:'b.
Thm* iso_pair('a;'b;P;rep;abs rep(a) = r  a = abs(r)
['a List;('a);is_list_rep;rep_list;abs_list;nil;<n:. @e:'a. true,0>]
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))


Generated subgoals:

1   iso_pair('a List;('a);is_list_rep;rep_list;abs_list)
1 step
2   rep_list(nil) = <n:. @e:'a. true,0>  ('a)
5 steps

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

(8steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc