dsimp
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
        { aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }
      else aig.mkConstCached false,
      assign⟧ =
    if h : (GetLsbTarget.mk expr idx).idx < (GetLsbTarget.mk expr idx).w then
      ⟦{ aig := aig, ref := (GetLsbTarget.mk expr idx).stream.getRef (GetLsbTarget.mk expr idx).idx h }, assign⟧
    else false
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
w✝ : Nat
expr : aig.RefStream w✝
idx : Nat
⊢ ⟦if h : idx < w✝ then { aig := aig, ref := expr.getRef idx h } else aig.mkConstCached false, assign⟧ =
    if h : idx < w✝ then ⟦{ aig := aig, ref := expr.getRef idx h }, assign⟧ else false