rcases target with ⟨lw, rw, lhs, rhs, ht⟩
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦{
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < target.rw then ⟦{ aig := aig, ref := target.rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := target.lhs.getRef (idx✝ - target.rw) ⋯ }, assign⟧
case mk.refl
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefStream lw✝
rw : aig.RefStream rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦{
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, stream := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, stream := ⋯ ▸ combined }).stream.getRef
            idx✝ hidx✝ },
      assign⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.getRef idx✝ hr }, assign⟧
    else
      let_fun this := ⋯;
      ⟦{ aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.getRef (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }, assign⟧