intro idx hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
input : IfInput aig w
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (ite aig input).aig, ref := (ite aig input).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 aig input).aig, ref := (ite aig input).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⟧