Nuprl - Proof: list iso 2

(37steps 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: list iso 2

1. 'a : S

type_definition((

'a)

;'a List;is_list_rep;rep_list)

By:	Unab [`type_definition`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

1 2. x' : 'a List
3. x'' : 'a List
4. rep_list('a;x') = rep_list('a;x'')
  x' = x''
9 steps

2 2. x : ('a)
3. is_list_rep(x)
  x':'a List. x = rep_list('a;x')
17 steps

3 2. x : ('a)
3. x':'a List. x = rep_list('a;x')
  is_list_rep(x)
8 steps

About:

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

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

1	2. x' : 'a List 3. x'' : 'a List 4. rep_list('a;x') = rep_list('a;x'') x' = x''	9 steps
2	2. x : ('a) 3. is_list_rep(x) x':'a List. x = rep_list('a;x')	17 steps
3	2. x : ('a) 3. x':'a List. x = rep_list('a;x') is_list_rep(x)	8 steps