simp only [mkNotCached]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
gate : aig.Ref
⊢ aig.decls.size ≤
    ((aig.mkConstCached true).aig.mkGateCached
            { lhs := { ref := (aig.mkConstCached true).ref, inv := false },
              rhs := { ref := gate.cast ⋯, inv := true } }).aig.decls.size