assumption
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
no goals