simp only [hsplit, decide_False, cond_false]
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    bif decide (idx < rw) then (eval assign rhs).getLsb idx else (eval assign lhs).getLsb (idx - rw)
w : Nat
assign : Assignment
lw rw : Nat
lhs : BVExpr lw
rhs : BVExpr rw
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < lw),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < rw),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < lw + rw
hsplit : ¬idx < rw
⊢ ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
        ref := { gate := ((go aig lhs).1.stream.getRef (idx - rw) ⋯).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (eval assign lhs).getLsb (idx - rw)