rw [LawfulOperator.denote_mem_prefix]
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{
        aig :=
          ((aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.mkNotCached
              { gate := input.discr.gate, hgate := ⋯ }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧
case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ ⟦{ aig := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig,
        ref := { gate := input.rhs.gate, hgate := ?e_y.e_y } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.rhs }, assign⟧

case e_y.e_y
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.TernaryInput
⊢ input.rhs.gate < (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).aig.decls.size