Who Cites seq cons?
seq_cons	Def  [x/ xs](i) == if i=0 x else xs(i-1) fi
	Thm*  A:Type, n:, x:A, xs:((n-1)A). [x/ xs]  nA
eq_int	Def  i=j == if i=j true ; false fi
	Thm*  i,j:. (i=j)

Syntax:

[x/ xs]

has structure:

seq_cons(x; xs)

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