split
case signExtend.inr
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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 < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
⊢ (if h : idx < originalWidth then
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧
    else
      ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
        assign.toAIGAssignment⟧) =
    if idx < originalWidth then (eval assign inner).getLsb idx else (eval assign inner).msb
case signExtend.inr.isTrue
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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 < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef idx ⋯ }, assign.toAIGAssignment⟧ =
    (eval assign inner).getLsb idx

case signExtend.inr.isFalse
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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 < v
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
hlt : 0 < originalWidth
h✝ : ¬idx < originalWidth
⊢ ⟦{ aig := (go aig inner).1.aig, ref := (go aig inner).1.stream.getRef (originalWidth - 1) ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign inner).msb