-(*
-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
-*)
-
-(*
- x n = n 0 ?
-x a (b (a c)) a 0 = 1 ? (b (a c)) 8
-x a (b d') a 0 = 1 ? (b d') 7
-x b (a c) b 0 = 1 ? (a c) 4
-x b (a c') b 0 = 1 ? (a c') 5
-
-c = 2
-c' = 3
-a 2 = 4 (* a c *)
-a 3 = 5 (* a c' *)
-d' = 6
-b 6 = 7 (* b d' *)
-b 4 = 8 (* b (a c) *)
-b 0 = 1
-a 0 = 1
-*)