structural ability Either a b where
left : a -> {Either a b} ()
right : b -> {Either a b} ()
structural type Either a b = Left a | Right b