Theorem: BitVec.add_eq_adc' (Smt/Reconstruct/BitVec/Bitblast.lean)

State before:
w : Nat
x y : BitVec w
⊢ x + y = (x.adc' y false).snd
Tactic:
rw [add_eq_adc, adc_eq_adc']
State after:
no goals