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

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