exact hstart
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
c : BitVec w
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

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

case m
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
c : BitVec w
start : Nat
hstart : start < aig.decls.size
⊢ Nat
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
assign : α → Bool
aig : AIG α
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
c : BitVec w
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig idx s c hidx).aig.decls.size