simp only [bitblast, eval_bin, BVBinPred.eval_eq]
case bin.eq
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs BVBinPred.eq rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs BVBinPred.eq rhs)
case bin.eq
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkEq (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs == BVExpr.eval assign rhs)