cases a
case one
a : binary
hb : a = binary.one
⊢ ¬a = binary.zero
case one.zero
hb : binary.zero = binary.one
⊢ ¬binary.zero = binary.zero

case one.one
hb : binary.one = binary.one
⊢ ¬binary.one = binary.zero