module F123 where



data A = A1 | A2
data B = B1 | B2

{-# CONTRACT h1 :: {x | noA2 x} -> {r | yesA2 r} #-}
h1 :: A -> A
h1 A1 = A2


noA2 A1 = True
noA2 A2 = False

yesA2 A1 = False
yesA2 A2 = True

f3 x y =  case y of
	     B1 -> f2 x y

f2 x y = case y of
            B1 -> f1 x

f1 x = h1 A2