split
case extract
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
⊢ (if h : lo + idx < w✝ then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧
    else false) =
    (eval assign inner).getLsb (lo + idx)
case extract.isTrue
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (lo + idx) ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb (lo + idx)

case extract.isFalse
w : Nat
assign : Assignment
w✝ hi lo : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < hi - lo + 1
this : idx ≤ hi - lo
h✝ : ¬lo + idx < w✝
⊢ false = (eval assign inner).getLsb (lo + idx)