dsimp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{
        aig :=
          (match input with
            | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).aig,
        ref :=
          (match input with
                | { discr := discr, lhs := lhs, rhs := rhs } => ite.go aig 0 ⋯ discr lhs rhs empty).stream.getRef
            idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).aig,
        ref := (ite.go aig 0 ⋯ input.discr input.lhs input.rhs empty).stream.getRef idx hidx },
      assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then
      ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧