apply mkOverflowBit.go_eq_carry
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkOverflowBit.go aig 0 ⋯ input.cin input.2.lhs input.2.rhs, assign⟧ =
    BitVec.carry input.w lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧
case hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx

case hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ∀ (idx : Nat) (hidx : idx < input.w), ⟦{ aig := aig, ref := input.2.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx

case hcin
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : OverflowInput aig
lhs rhs : BitVec input.w
assign : α → Bool
hleft :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright :
  ∀ (idx : Nat) (hidx : idx < input.w),
    ⟦{ aig := aig, ref := input.stream.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦{ aig := aig, ref := input.cin }, assign⟧ = BitVec.carry 0 lhs rhs ⟦{ aig := aig, ref := input.cin }, assign⟧