rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast (bitblast aig lhs).aig rhs).aig, ref := ((bitblast aig lhs).stream.getRef idx hidx).cast ⋯ },
        assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)
case bin.or
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ (⟦{ aig := (bitblast aig lhs).aig, ref := (bitblast aig lhs).stream.getRef idx hidx }, assign.toAIGAssignment⟧ ||
      (eval assign rhs).getLsb idx) =
    ((eval assign lhs).getLsb idx || (eval assign rhs).getLsb idx)