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