Def		xL.P(x)	[list_exists_2]
Def		||	[list_length]
Def			[nat]	int 1
Def		x:A. B(x)	[all]	core
Def		ij	[ge]	core
Def		||as||	[length]	list 1
Def		Discrete{T}	[discrete]	discrete jlc
Def		P Q	[implies]	core
Def		null(as)	[null]	list 1
Def			[bool]	bool 1
Def		{T}	[equivalence]	core 3 jlc
Def		{T=}	[discrete_equality]	discrete jlc
Def		P Q	[iff]	core
Def		x:A. B(x)	[exists]	core
Def		remove(eq;x;L)	[remove]
Def		filter(f;L)	[filter]
Def		SqStable(P)	[sq_stable]	core
Def		Dec(P)	[decidable]	core
Def		hd(l)	[hd]	list 1
Def		a b	[nequal]	core
Def		Prop	[prop]	core
Def		AB	[le]	core
Def		A	[not]	core
Def		disjoint(eq;L1;L2)	[disjoint]
Def		disjoint(eq;L;M)	[disjoint2]
Def		as @ bs	[append]	list 1
Def		A & B	[cand]	core
Def		L1(~eq)L2	[list_iso]
Def		{T}	[guard]	core
Def		(~eq)	[list_iso_2]
Def		L(eq)M	[is_intersection]
Def		L1(eq)L2	[sublist]
Def		(eq)	[sublist_2]
Def		x(eq) L	[is_member]
Def		xL.P(x)	[list_all]
Def		xL.P(x)	[list_all_2]
Def		xL.P(x)	[list_exists]
Def		= b	[letrec_body]	lambda jlc
Def		x b(x)	[letrec_arg]	lambda jlc
Def		(letrec f b(f))	[letrec]	lambda jlc
Def		if b t else f fi	[ifthenelse]	bool 1
Def		true	[btrue]	bool 1
Def		false	[bfalse]	bool 1
Def		P & Q	[and]	core
Def		True	[true]	core
Def		pq	[band]	bool 1
Def		P Q	[or]	core
Def		False	[false]	core
Def		p q	[bor]	bool 1
Def		b	[bnot]	bool 1
Def		b	[assert]	bool 1
Def		P Q	[rev_implies]	core
Def		T	[squash]	core

About: