'a:S. equal(nil,abs_list(pair((
n:hnum. select(e:'a. t)),0)))'a,'b:S, P:('b
), rep:('a'b), abs:('b'a), a:'a, r:'b.
Thm* iso_pair('a;'b;P;rep;abs)
rep(a) = r a = abs(r)'a:S. iso_pair('a List;(
'a)
;is_list_rep;rep_list;abs_list)'a:S. equal(arb,select(x:'a. t))