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

State before:
⊢ @adc = @adc'
Tactic:
funext x y c
State after:
case h.h.h
x : Nat
y c : BitVec x
⊢ y.adc c = y.adc' c

State before:
case h.h.h
x : Nat
y c : BitVec x
⊢ y.adc c = y.adc' c
Tactic:
simp only [adc, adc', adcb_eq_adcb']
State after:
no goals