T:Type, L:T List, P:(T
T
). count(x < y in L | P(x,y)) 
n:, f:(n
). (x:n. 0
f(x)) 
0sum(f(x) | x < n)| Theorem | Name |
| T:Type, L:T List, P:(TT). count(x < y in L | P(x,y)) | [count_pairs_wf] |
| cites the following: | |
| n:, f:(n). (x:n. 0f(x)) 0sum(f(x) | x < n) | [non_neg_sum] |