idris-0.1.5: lib/either.idr

data Either A B = Left A | Right B;

choose : (x:Bool) -> Either (so (not x)) (so x);
choose False = Left oh;
choose True = Right oh;