rw [Bool.eq_iff_iff]
α : 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
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.stream;
      RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
      assign⟧ =
    (lhs == rhs)
α : 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
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.stream;
        RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
        assign⟧ =
      true ↔
    (lhs == rhs) = true