rw [← beq_as_aig]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkBEqCached input, assign⟧ =
    (⟦{ aig := aig, ref := input.lhs }, assign⟧ == ⟦{ aig := aig, ref := input.rhs }, assign⟧)
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkBEqCached input, assign⟧ =
    (!(⟦{ aig := aig, ref := input.lhs }, assign⟧ && !⟦{ aig := aig, ref := input.rhs }, assign⟧) &&
      !(!⟦{ aig := aig, ref := input.lhs }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧))