Theorem: Bool.atLeastTwo_eq_halfAdder (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean)

State before:
α : Type ?u.21012
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
lhsBit rhsBit carry : Bool
⊢ lhsBit.atLeastTwo rhsBit carry = (xor lhsBit rhsBit && carry || lhsBit && rhsBit)
Tactic:
cases lhsBit <;> cases rhsBit <;> cases carry <;> decide
State after:
no goals