theorem
Std.Tactic.BVDecide.BVPred.mkEq_denote_eq
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(pair : aig.BinaryRefVec w)
(assign : α → Bool)
(lhs : BitVec w)
(rhs : BitVec w)
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx)
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx)
:
⟦assign, Std.Tactic.BVDecide.BVPred.mkEq aig pair⟧ = (lhs == rhs)