Who Cites is intersection?
is_intersection	Def L(eq)M == xL.x(eq) M
	Thm* T:Type, eq:{T}, L,M:T List. L(eq)M Type
is_member	Def x(eq) L == (letrec is_member x eq L = (Case of L; nil false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L)
	Thm* T:Type, eq:(TT), u:T. u(eq) nil
	Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L
assert	Def b == if b True else False fi
	Thm* b:. b Prop
list_exists	Def xL.P(x) == (letrec list_exists L = (Case of L; nil False ; h.t P(h) list_exists(t)) ) (L)
	Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type
letrec_body	Def = b == b
letrec_arg	Def x b(x) (x) == b(x)
letrec	Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)

Syntax:

L(eq)M

has structure:

is_intersection(eq; L; M)

About: