Who Cites member-paren?
member-paren	Def member-paren(x,y.E(x;y);i;s) == (xs.InjCase(x; a. E(a;i), E(a;i)))
l_bexists	Def (xL.P(x)) == reduce(x,b. P(x) b;false;L)
	Thm* T:Type, L:T List, P:(T). (xL.P(x))
bor	Def p q == if p true else q fi
	Thm* p,q:. (p q)
reduce	Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B

Syntax:

member-paren(x,y.E(x;y);i;s)

has structure:

member-paren(x,y.E(x;y); i; s)

About: