Nuprl - Definition Cascade for unzip

	Who Cites unzip?

unzip	`Def unzip(as) == < map(p.1of(p);as),map(p.2of(p);as) >`

	`Thm* T1,T2:Type, as:(T1T2) List. unzip(as) (T1 List)(T2 List)`

pi2	`Def 2of(t) == t.2`

	`Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))`

map	`Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive)`

	`Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List`

	`Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List`

pi1	`Def 1of(t) == t.1`

	`Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A`

About: