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*
j == if i < j true ; false fi
Thm* i,j:. i < j 
| firstn |
Def firstn(n;as)
== Case of as; nil nil ; a.as' if 0 < n a.firstn(n-1;as') else nil fi
(recursive)
Thm* |
| lt_int |
Def i < j == if i < j true ; false fi
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |