rw [← hleft, ← hright]
case mp.pred
α : 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 :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ lhs.getLsb ↑i✝ = rhs.getLsb ↑i✝
case mp.pred
α : 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 :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧

case mp.pred.hidx
α : 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 :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : 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 :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : 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 :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w