Sort u →
  {α : Type} →
    [inst : Hashable α] →
      [inst_1 : DecidableEq α] →
        {aig : Std.Sat.AIG α} →
          {len : ℕ} →
            Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig len →
              {α' : Type} →
                [inst' : Hashable α'] →
                  [inst'_1 : DecidableEq α'] →
                    {aig' : Std.Sat.AIG α'} →
                      {len' : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig' len' → Sort u