1 2 3 4 5 6 7
Definition Berry := [x,y,z:bool] Cases x y z of true false _ => O | false _ true => (S O) | _ true false => (S (S O)) end.