cases op with
| eq =>
  simp only [bitblast, eval_bin, BVBinPred.eval_eq]
  rw [mkEq_denote_eq_eval_beq]
  . intros
    rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
    . simp
      rw [BVExpr.bitblast_denote_eq_eval_getLsb]
    . simp [Ref.hgate]
  . intros
    simp
| ult =>
  simp only [bitblast, eval_bin, BVBinPred.eval_ult]
  rw [mkUlt_denote_eq_eval_ult]
  . intros
    rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
    . simp
      rw [BVExpr.bitblast_denote_eq_eval_getLsb]
    . simp [Ref.hgate]
  . intros
    simp
case bin
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs op rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs op rhs)
no goals