Sort u →
  {α : Type} →
    [inst : Hashable α] →
      [inst_1 : DecidableEq α] →
        {aig : Std.Sat.AIG α} →
          {w : ℕ} →
            aig.ShiftTarget w →
              {α' : Type} →
                [inst' : Hashable α'] →
                  [inst'_1 : DecidableEq α'] → {aig' : Std.Sat.AIG α'} → {w' : ℕ} → aig'.ShiftTarget w' → Sort u