apply go_le_size
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig curr hcurr cin s lhs rhs).aig.decls.size
no goals