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`

sublist	`Def L1 L2 == f:(\|\|L1\|\|\|\|L2\|\|). increasing(f;\|\|L1\|\|) & (j:\|\|L1\|\|. L1[j] = L2[(f(j))] T)`

	`Thm* T:Type, L1,L2:T List. L1 L2 Prop`

About: