let pred = \n. iszero n 0 (length (tail (n (\p. make_list junk p) empty))) in
let leq = \m n. iszero(n pred m) in
let eq = \m n. and (leq m n)(leq n m) in
let pred = \n. iszero n 0 (length (tail (n (\p. make_list junk p) empty))) in
let leq = \m n. iszero(n pred m) in
let eq = \m n. and (leq m n)(leq n m) in