Who Cites fappend?
fappend	Def f[n:=x](i) == if i=n x else f(i) fi
	Thm* n,m:, f:(nm), x:m. f[n:=x]  (n+1)m
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)

Syntax:

f[n:=x]

has structure:

fappend(f; n; x)

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