cases op with
| eq =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := mkEq)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    assumption
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    assumption
| ult =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := mkUlt)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    assumption
  . apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
    apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
    assumption
case bin
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs : BVExpr w✝
op : BVBinPred
rhs : BVExpr w✝
⊢ let_fun this := ⋯;
  (bitblast aig (bin lhs op rhs)).aig.decls[idx] = aig.decls[idx]
no goals