-(*
-0 = snd
-
- x y = y 0 a y = k k z = z 0 c y = k y u = u h1 h2 0 h2 a = h3
-1 x a c 1 a 0 c 1 k c 1 c 0 1 k 1 k 1 k
-2 x a y 2 a 0 y 2 k y 2 y 0 2 y 0 2 h2 0 2 h3
-3 x b y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 (\u. u h1 h2 0) 3 b 0 (\u. u h1 (\w.h3) 0)
-4 x b c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c
-5 x (b e) 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0
-6 y y 6 y y 6 y y 6 y y 6 y y 6 h1 h1 h2 0 h2 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0
-
- l2 _ = l3
-b u = u l1 l2 0 e _ _ _ _ = f l3 n = n j 0
-1 k 1 k 1 k
-2 h3 2 h3 2 h3
-3 l2 0 (\u. u h1 (\w. h3) 0) 3 l3 (\u. u h1 (\w. h3) 0) 3 j h1 (\w. h3) 0 0
-4 l2 0 c 4 l3 c 4 c j 0
-5 e l1 l2 0 0 5 f 5 f
-6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0
-*)