{α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → (n : ℕ) → aig.RefVec w → (curr : ℕ) ×' (_ : curr ≤ n) ×' aig.RefVec (w * curr) → aig.RefVec (w * n)