simp only [getRef, append]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ (lhs.append rhs).getRef idx hidx = if h : idx < lw then lhs.getRef idx h else rhs.getRef (idx - lw) ⋯
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }