rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := (input.lhs.cast ⋯).getRef idx hidx },
      assign⟧ =
    lhs.getLsb idx
case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((input.lhs.cast ⋯).getRef idx hidx).gate, hgate := ?e_a.hleft✝ } },
      assign⟧ =
    lhs.getLsb idx

case e_a.hleft
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).getRef idx hidx).gate < (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size