apply Nat.lt_of_lt_of_le
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
start : Nat
hstart : start < aig.decls.size
⊢ start < (go aig w input newWidth curr hcurr s).aig.decls.size
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig w input newWidth curr hcurr s).aig.decls.size

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
w : Nat
input : aig.RefStream w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefStream curr
start : Nat
hstart : start < aig.decls.size
⊢ Nat