match op with
| .not =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastNot)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
| .shiftLeftConst _ =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftLeftConst)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
| .shiftRightConst _ =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastShiftRightConst)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
| .rotateLeft _ =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastRotateLeft)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
| .rotateRight _ =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastRotateRight)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
| .arithShiftRightConst _ =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastArithShiftRightConst)]
  rw [ih]
  apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (go aig expr).property
case un
w idx w✝ : Nat
op : BVUnOp
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (un op expr)).val.aig.decls.size
⊢ (go aig (un op expr)).val.aig.decls[idx] = aig.decls[idx]
no goals