Nuprl - Some Definitions

	Some definitions of interest.

append	`Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)`

	`Thm* T:Type, as,bs:T List. (as @ bs) T List`

iff	`Def P Q == (P Q) & (P Q)`

	`Thm* A,B:Prop. (A B) Prop`

l_disjoint	`Def l_disjoint(T;l1;l2) == x:T. ((x l1) & (x l2))`

	`Thm* T:Type, l,l':T List. l_disjoint(T;l;l') Prop`

l_member	`Def (x l) == i:. i < \|\|l\|\| & x = l[i] T`

	`Thm* T:Type, x:T, l:T List. (x l) Prop`

About: