have h1 := entry.ref.hgate
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size