Thm* x,y:, as:T*. nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as) nth_tl_lem1

Thm* y:, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) nth_tl_lem0

Thm* x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]]) firstn_lem1

In prior sections: int 1 bool 1 int 2 list 1 finite sets