Who Cites col?
col	Def Collection(T) == TProp
	Thm* T:Type{i'}. col{i:l}(T) Type{i'}
col_list_prod	Def col_list_prod(l)(x) == ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])
	Thm* T:Type, l:Collection(T) List. col_list_prod(l) Collection(T List)
col_member	Def x c == c(x)
	Thm* T:Type, x:T, c:Collection(T). x c Prop
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
length	Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
nat	Def == {i:| 0i }
	Thm* Type
select	Def l[i] == hd(nth_tl(i;l))
	Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop
le	Def AB == B < A
	Thm* i,j:. (ij) Prop
nth_tl	Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi (recursive)
	Thm* A:Type, as:A List, i:. nth_tl(i;as) A List
hd	Def hd(l) == Case of l; nil "?" ; h.t h
	Thm* A:Type, l:A List. ||l||1 hd(l) A
not	Def A == A False
	Thm* A:Prop. (A) Prop
tl	Def tl(l) == Case of l; nil nil ; h.t t
	Thm* A:Type, l:A List. tl(l) A List
le_int	Def ij == j < i
	Thm* i,j:. (ij)
lt_int	Def i < j == if i < j true ; false fi
	Thm* i,j:. (i < j)
bnot	Def b == if b false else true fi
	Thm* b:. b

About: