match op with
| .and | .or | .xor =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := AIG.RefStream.zip)]
  rw [rih, lih]
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (bitblast.go aig lhs).property
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . apply Nat.le_trans
      . exact (bitblast.go aig lhs).property
      . exact (go (go aig lhs).1.aig rhs).property
| .add =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastAdd)]
  rw [rih, lih]
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (bitblast.go aig lhs).property
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . apply Nat.le_trans
      . exact (bitblast.go aig lhs).property
      . exact (go (go aig lhs).1.aig rhs).property
case bin
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin op rhs)).val.aig.decls.size
⊢ (go aig (lhs.bin op rhs)).val.aig.decls[idx] = aig.decls[idx]
no goals