Who Cites list member type?
list_member_type	Def  xs == {a:A| a  xs }
	Thm*  A:Type, xs:A List. xs  Type
is_list_mem	Def  a  xs == Case of xs; nil  False ; x.ys  a = x  A  (a  ys) Def  (recursive)
	Thm*  A:Type, a:A, xs:A List. (a  xs)  Prop

Syntax:

xs

has structure:

list_member_type(A; xs)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html