apply go_le_size
case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
no goals