Fail Type match 0 with
     | x => 0
     | O => 1
     end.