. exact h
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ Nat
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size