rw [AIG.LawfulStreamOperator.decl_eq (f := BVExpr.bitblast)]
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size
case bin.eq
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ (BVExpr.bitblast aig lhs).aig.decls[idx] = aig.decls[idx]

case bin.eq.h1
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast aig lhs).aig.decls.size

case bin.eq.h2
idx : Nat
aig : AIG BVBit
h : idx < aig.decls.size
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ idx < (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig.decls.size