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