simp only [true_iff, false_iff] at *
case one
a : binary
hb : binary.one = binary.one ↔ a = binary.one
⊢ binary.one = binary.zero ↔ a = binary.zero
case one
a : binary
hb : a = binary.one
⊢ ¬a = binary.zero