Theorem: substructure_unit_1 (Test/Bv/Substructure.lean)

State before:
x y z : BitVec 8
⊢ x = y ∧ y = z ↔ ¬(¬x = y ∨ ¬y = z)
Tactic:
bv_decide
State after:
no goals