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: