intro h idx hidx
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧