apply AIG.LawfulOperator.le_size
case isTrue
w : Nat
aig : AIG BVBit
idx : Nat
s : aig.RefStream idx
a : Nat
hidx : idx ≤ w
h✝ : idx < w
⊢ aig.decls.size ≤ (aig.mkAtomCached (BVBit.mk a ⟨idx, h✝⟩)).aig.decls.size
no goals