Theorem: AIG.ofBoolExprCached.go_decls_size_le (LeanSAT/AIG/BoolExprCached.lean)

State before:
α β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
expr : BoolExpr α
aig : AIG β
⊢ aig.decls.size ≤ (go expr aig atomHandler).val.aig.decls.size
Tactic:
exact (ofBoolExprCached.go expr aig atomHandler).property
State after:
no goals