{α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) →
        (w : ℕ) →
          aig.RefVec w → (newWidth curr : ℕ) → curr ≤ newWidth → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α newWidth