cases g <;> simp [go, Gate.eval, lih, rih]
case gate
α✝ β : Type
inst✝⁶ : BEq β
inst✝⁵ : Hashable β
inst✝⁴ : DecidableEq β
atomHandler : AIG β → α✝ → Entrypoint β
inst✝³ : LawfulOperator β (fun x => α✝) atomHandler
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
g : Gate
lhs rhs : BoolExpr α
lih : ∀ (aig : AIG α), ⟦(go lhs aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign lhs
rih : ∀ (aig : AIG α), ⟦(go rhs aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign rhs
aig : AIG α
⊢ ⟦(go (BoolExpr.gate g lhs rhs) aig mkAtomCached).val, assign⟧ = BoolExpr.eval assign (BoolExpr.gate g lhs rhs)
no goals