Def	< x >	[col_singleton]
Def	< >	[col_none]
Def	c1 = c2	[col_equal]
Def	Collection(T)	[col]
Def	c1 c2	[col_le]
Def	< x c | P(x) >	[col_filter]
Def	i:I. C(i)	[col_union]
Def	< f(x) | x c >	[col_map]
Def	a + b	[col_add]
Def	(xc.f(x))	[col_accum]
Def	col_list_prod(l)	[col_list_prod]
Def	(xc.P(x))	[col_all]
Def	Prop	[prop]	core
Def	False	[false]	core
Def	x c	[col_member]
Def	P Q	[iff]	core
Def	x:A. B(x)	[all]	core
Def	P Q	[implies]	core
Def	P & Q	[and]	core
Def	x:A. B(x)	[exists]	core
Def	P Q	[or]	core
Def	l[i]	[select]	list 1
Def	||as||	[length]	list 1
Def		[nat]	int 1
Def	A & B	[cand]	core
Def	P Q	[rev_implies]	core
Def	nth_tl(n;as)	[nth_tl]	list 1
Def	hd(l)	[hd]	list 1
Def	AB	[le]	core
Def	tl(l)	[tl]	list 1
Def	ij	[le_int]	bool 1
Def	A	[not]	core
Def	i < j	[lt_int]	bool 1
Def	b	[bnot]	bool 1

About: