rw [if_as_bool]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦aig.mkIfCached input, assign⟧ =
    if ⟦{ aig := aig, ref := input.discr }, assign⟧ = true then ⟦{ aig := aig, ref := input.lhs }, assign⟧
    else ⟦{ aig := aig, ref := input.rhs }, assign⟧
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦aig.mkIfCached input, assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧ ||
      !⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.rhs }, assign⟧)