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