Nuprl - Some Definitions

	Some definitions of interest.

term_closed	`Def closed(t) == s,v:Term. t[s/v] = t`

	`Thm* t:Term. closed(t) Prop`

termof	`Def A Term == {t:Term\| t IN A }`

	`Thm* (A Term) Type`

About: