. simp
case e_x
α : 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 := (aig.mkAndCached { lhs := input.discr, rhs := input.lhs }).ref.gate, hgate := ?e_x } },
      assign⟧ =
    (⟦{ aig := aig, ref := input.discr }, assign⟧ && ⟦{ aig := aig, ref := input.lhs }, assign⟧)

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