Def firstn(n;as) == Case of as; nil nil ; a.as' if 0 < n a.firstn(n-1;as') else nil fi (recursive)

Thm* A:Type, as:A*, n:. firstn(n;as) A*

Def AB == B < A

Thm* i,j:. ij Prop

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

Def i < j == if i < j true ; false fi

Thm* i,j:. i < j

Def A == A False

Thm* A:Prop. (A) Prop