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

State before:
a : Bool
b c : BitVec 32
h1 : b < c ↔ a = true
h2 : a = true
⊢ b < c
Tactic:
bv_decide
State after:
no goals