simp
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false
no goals