apply lt_size_of_lt_aig_size
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefStreamEntry α len
inst✝ : LawfulStreamOperator α β fun {len} => f
len start : Nat
assign : α → Bool
aig : AIG α
input : β aig len
h : start < aig.decls.size
⊢ start < aig.decls.size