module CatchAllAbsurdPattern where

data Zero : Set where

record One : Set where

data Three : Set where
  zero : Three
  one  : Three
  two  : Three

Eq : Three -> Three -> Set
Eq zero zero = One
Eq one one = One
Eq two two = One
Eq _ _ = Zero

sym : forall x y -> Eq x y -> Eq y x
sym zero zero H = H
sym one  one  H = H
sym two  two  H = H
sym _    _   ()