x:
, as:T*. x < ||as|| 
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
firstn_lem1
nil ; a.as' if 0 < 
n a.firstn(n-1;as') else nil fi
(recursive)
Thm* x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]])
firstn_lem1
Thm* as:T*. firstn(||as||;as) = as firstn_lem0
In prior sections: list 1