zip(Nil,      y  )       = Nil
zip(Cons(a,x),Nil)       = Nil
zip(Cons(a,x),Cons(b,y)) = Cons(Pair(a,b),zip(x,y))

snoc(Nil,y)       = Cons(y,Nil)
snoc(Cons(a,x),y) = Cons(a,snoc(x,y))

f(A(x))   = A(f(x))
f(B(x,y)) = B(f(x),f(y))
f(C)      = C

fst(Pair(x,y)) = x
snd(Pair(x,y)) = y
idPair(Pair(x,y)) = Pair(x,y)

inc(x) = S(x)
dec(S(x)) = x

not(True)  = False
not(False) = True

rev(Node(x,y)) = Node(rev(y),rev(x))
rev(Leaf(x))   = idB(x)

idB(True)  = True
idB(False) = False

idNat(S(x)) = S(idNat(x))
idNat(Z)    = Z

add(S(x),y) = S(add(x,y))
add(Z,y)    = idNat(y)

nil(x) = Nil

half(S(S(x))) = S(half(x))
half(S(Z))    = Z
half(Z)       = Z

subT(Br(Br(x,y),z)) = Just(Br(x,y))
subT(Br(Lf,x))      = subT(x)
subT(Lf)            = Nothing

sIf(Var(v))   = Var(v)
sIf(Const(i)) = Const(i)
sIf(True)  = True
sIf(False) = False
sIf(Rel(op,e1,e2)) = Rel(op, sIf(e1), sIf(e2))
sIf(Not(e)) = Not(sIf(e))
sIf(App(f,e)) = App(f,sIf(e))
sIf(If(True,e1,e2))  = sIf(e1)
sIf(If(False,e1,e2)) = sIf(e1)
sIf(If(e,e1,e2))     = If(sIf(e),sIf(e1),sIf(e2))
