cases pred with
| bin lhs op rhs =>
  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
| getLsb expr idx =>
  simp only [bitblast]
  rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
  rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
  apply AIG.LawfulStreamOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
  assumption
idx : Nat
aig : AIG BVBit
pred : BVPred
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (bitblast aig pred).aig.decls[idx] = aig.decls[idx]
no goals