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

State before:
⊢ adcb = adcb'
Tactic:
funext x y c
State after:
case h.h.h
x y c : Bool
⊢ adcb x y c = adcb' x y c

State before:
case h.h.h
x y c : Bool
⊢ adcb x y c = adcb' x y c
Tactic:
cases x <;> cases y <;> cases c <;> rfl
State after:
no goals